Modular Programming Language Development - Publications by Topic

Publications

publications by year · publications by type · publications by topic

Compilers

[J1]	Calculating correct compilers Patrick Bahr and Graham Hutton Journal of Functional Programming, 25, 2015. bib doi url Paper Appendix Coq Proofs
[C4]	Calculating Certified Compilers for Non-deterministic Languages Patrick Bahr Mathematics of Program Construction, p. 159-186, 2015. bib doi url Paper Slides Coq Proofs
[C2]	Proving Correctness of Compilers Using Structured Graphs Patrick Bahr Functional and Logic Programming, p. 221-237, 2014. bib doi url Paper Technical Report Slides Coq Proofs Coq Proofs

Domain-specific Languages

[C6]	Certified Symbolic Management of Financial Multi-party Contracts Patrick Bahr, Jost Berthold and Martin Elsman Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, p. 315-327, 2015. bib doi url Paper Slides Coq Proofs
[L1]	Towards Certified Management of Financial Contracts Patrick Bahr, Jost Berthold and Martin Elsman Proceedings of the 26th Nordic Workshop on Programming Theory, NWPT '14, 2014. bib Extended Abstract Slides Source Code & Coq Proofs
[T1]	Modular Implementation of Programming Languages and a Partial-Order Approach to Infinitary Rewriting Patrick Bahr Ph.D. Dissertation, Department of Computer Science, University of Copenhagen, 2012. bib Dissertation Slides

Formal Verification

[I1]	Cutting Out Continuations Graham Hutton and Patrick Bahr A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday bib doi url Paper Coq Proofs
[J1]	Calculating correct compilers Patrick Bahr and Graham Hutton Journal of Functional Programming, 25, 2015. bib doi url Paper Appendix Coq Proofs
[C6]	Certified Symbolic Management of Financial Multi-party Contracts Patrick Bahr, Jost Berthold and Martin Elsman Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, p. 315-327, 2015. bib doi url Paper Slides Coq Proofs
[C4]	Calculating Certified Compilers for Non-deterministic Languages Patrick Bahr Mathematics of Program Construction, p. 159-186, 2015. bib doi url Paper Slides Coq Proofs
[L1]	Towards Certified Management of Financial Contracts Patrick Bahr, Jost Berthold and Martin Elsman Proceedings of the 26th Nordic Workshop on Programming Theory, NWPT '14, 2014. bib Extended Abstract Slides Source Code & Coq Proofs
[C2]	Proving Correctness of Compilers Using Structured Graphs Patrick Bahr Functional and Logic Programming, p. 221-237, 2014. bib doi url Paper Technical Report Slides Coq Proofs Coq Proofs

Recursion Schemes

[C3]	Generalising Tree Traversals to DAGs: Exploiting Sharing without the Pain Patrick Bahr and Emil Axelsson Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, p. 27-38, 2015. bib doi url Paper Technical Report Slides Hackage Source Code
[W4]	Composing and Decomposing Data Types: A Closed Type Families Implementation of Data Types à La Carte Patrick Bahr Proceedings of the 10th ACM SIGPLAN Workshop on Generic Programming, p. 71-82, 2014. bib doi url Paper Slides Hackage Source Code
[W3]	Programming macro tree transducers Patrick Bahr and Laurence E. Day Proceedings of the 9th ACM SIGPLAN Workshop on Generic Programming, p. 61-72, 2013. bib doi url Paper Appendix Slides Hackage Source Code
[C1]	Modular Tree Automata Patrick Bahr Mathematics of Program Construction, p. 263-299, 2012. bib doi url Paper Slides Hackage Source Code
[W2]	Parametric Compositional Data Types Patrick Bahr and Tom Hvitved Proceedings Fourth Workshop on Mathematically Structured Functional Programming, p. 3-24, 2012. bib doi Paper Slides Hackage Source Code
[W1]	Compositional data types Patrick Bahr and Tom Hvitved Proceedings of the seventh ACM SIGPLAN workshop on Generic programming, p. 83-94, 2011. bib doi url Paper Slides Hackage Source Code

Rewriting

[T1]	Modular Implementation of Programming Languages and a Partial-Order Approach to Infinitary Rewriting Patrick Bahr Ph.D. Dissertation, Department of Computer Science, University of Copenhagen, 2012. bib Dissertation Slides

Type Systems

[C6]	Certified Symbolic Management of Financial Multi-party Contracts Patrick Bahr, Jost Berthold and Martin Elsman Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, p. 315-327, 2015. bib doi url Paper Slides Coq Proofs
[C5]	Type Families with Class, Type Classes with Family Alejandro Serrano, Jurriaan Hage and Patrick Bahr Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, p. 129-140, 2015. bib doi url Paper Extended Version Slides
[W4]	Composing and Decomposing Data Types: A Closed Type Families Implementation of Data Types à La Carte Patrick Bahr Proceedings of the 10th ACM SIGPLAN Workshop on Generic Programming, p. 71-82, 2014. bib doi url Paper Slides Hackage Source Code
[W3]	Programming macro tree transducers Patrick Bahr and Laurence E. Day Proceedings of the 9th ACM SIGPLAN Workshop on Generic Programming, p. 61-72, 2013. bib doi url Paper Appendix Slides Hackage Source Code
[T1]	Modular Implementation of Programming Languages and a Partial-Order Approach to Infinitary Rewriting Patrick Bahr Ph.D. Dissertation, Department of Computer Science, University of Copenhagen, 2012. bib Dissertation Slides
[W2]	Parametric Compositional Data Types Patrick Bahr and Tom Hvitved Proceedings Fourth Workshop on Mathematically Structured Functional Programming, p. 3-24, 2012. bib doi Paper Slides Hackage Source Code
[W1]	Compositional data types Patrick Bahr and Tom Hvitved Proceedings of the seventh ACM SIGPLAN workshop on Generic programming, p. 83-94, 2011. bib doi url Paper Slides Hackage Source Code