Publications

Each publication employs Beluga syntax for the most recent release at time of writing. If you have trouble discerning Beluga code from older releases, consult the legacy syntax for clarification.

consult the legacy syntax for clarification.

• Jonas Kaiser, Brigitte Pientka, and Gert Smolka. Relating System F and Lambda2: A Case Study in Coq, Abella, and Beluga, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD'17); more details, in particular the code for each case study can be found in the online repository.
• Aina Linn Georges, Agata Murawska, Shawn Otis, Brigitte Pientka. Lincx: A Linear Logical Framework with First-Class Contexts, 26th European Symposium on Programming (ESOP'17), 2017
• Francisco Ferreira, Brigitte Pientka. Programs Using Syntax with First-Class Binders, 26th European Symposium on Programming (ESOP'17), 2017
• Amy Felty, Alberto Momigliano, Brigitte Pientka. Benchmarks for Reasoning with Syntax Trees Containing Binders and Contexts of Assumptions accepted in Mathematical Structures in Computer Science (MSCS), 2017.
• David Thibodeau, Andrew Cave, Brigitte Pientka. Indexed Codata Types (submitted March 2016), International Conference on Functional Programming (ICFP'16)
• Rohan Jacob-Rao, Andrew Cave and Brigitte Pientka. Mechanizing Proofs about Mendler-Recursion, 11th Workshop Logical Frameworks and Meta-languages (LFMTP'16): Theory and Practice, 2016
• Brigitte Pientka, Andrew Cave. Inductive Beluga: Programming Proofs (System Description), CADE-25, 2015.
• Andrew Cave and Brigitte Pientka. A Case Study on Logical Relations using Contextual Types, LFMTP'15
• Brigitte Pientka, Andreas Abel. Structural Recursion over Contextual Objects, (Long version, draft from Feb 2015), TLCA'15, 2015
• Amy Felty, Alberto Momigliano, Brigitte Pientka. The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 2 - A Survey (including the electronic appendix), Journal of Automated Reasoning, 55(4): 307-372, 2015.
• Olivier Savary-Belanger, Stefan Monnier and Brigitte Pientka. Programming type-safe transformations using higher-order abstract syntax, pdf + Beluga code, Journal of Formalized Reasoning. 8(1): 49-91, 2015. (This is the long and revised version of the CPP'13 paper)
• Andreas Abel, Brigitte Pientka, Anton Setzer, David Thibodeau. Unnesting of Copatterns, Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA'14), LNCS 8560, pages 31-45, Springer, 2014.
• Amy Felty, Alberto Momigliano, Brigitte Pientka. The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1 - A Common Infrastructure, CoRR abs/1503.06095, 2015.
• Andreas Abel and Brigitte Pientka. Well-founded Recursion with Copatterns and Sized Types, Extended journal version of the ICFP'13 conference paper, Journal of Functional Programming, 2016, vol. 26.
• Francisco Ferreira, Brigitte Pientka, Bidirectional Elaboration of Dependently Typed Programs, PPDP'14 (long version including soundness proof)
• Anton Setzer, Andreas Abel, Brigitte Pientka and David Thibodeau. Unnesting of Copatterns, TLCA'14
• Andrew Cave, Francisco Ferreira, Prakash Panangaden, and Brigitte Pientka. Fair reactive programming, 41th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'14), (Long version).
• Olivier Savary-Belanger, Stefan Monnier and Brigitte Pientka. Programming type-safe transformations using higher-order abstract syntax, 3rd International Conference on Certified Programs and Proofs (CPP'13). (code)
• Francisco Ferreira, Stefan Monnier, Brigitte Pientka. Compiling contextual objects: Bringing Higher-Order Abstract Syntax to Programmers, 7th ACM SIGPLAN Workshop on Programming Languages meets Program Verification (PLPV'13).
• Andreas Abel, Brigitte Pientka, David Thibodeau, Anton Setzer. Copatterns: Programming Infinite Structures by Observations, 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'13)
• Brigitte Pientka. An insider's look at LF type reconstruction:Everything you (n)ever wanted to know, Journal of Functional Programming, Jan 2013
• Andrew Cave and Brigitte Pientka. First-class substitutions in contextual type theory, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'13).
• Brigitte Pientka. Coverage checking contextual objects, draft June 2012, (tar-ball with Beluga examples)
• Andrew Cave and Brigitte Pientka. Programming with Binders and Indexed Data-types, 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12).
• Mathieu Boespflug and Brigitte Pientka. Multi-level Contextual Type Theory, 6th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'11) (long version).
• Andreas Abel and Brigitte Pientka. Higher-order dynamic pattern unification for dependent types and records, 10th Conference on Typed Lambda Calculi and Applications (TLCA'11). (long version)
• Brigitte Pientka and Joshua Dunfield. Covering all bases: design and implementation of case analysis for contextual objects. Technical report, Oct 2010. (pdf, electronic appendix, electronic appendix (tar-ball))
• Amy Felty and Brigitte Pientka. Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. In First International Conference on Interactive Theorem Proving (ITP'10), Lecture Notes in Computer Science (LNCS), vol 6172, page 227-242, Springer, 2010. (abstract) (pdf) (appendix)
• Brigitte Pientka and Joshua Dunfield. Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description). In 5th International Joint Conference on Automated Reasoning (IJCAR'10), Lecture Notes in Computer Science (LNCS), vol 6173, page 15-21, Springer, 2010. (abstract) (pdf)
• Andreas Abel and Brigitte Pientka. Explicit substitutions for contextual type theory. In 5th International Workshop on Logical Frameworks: Theory and Practice (LFMTP'10), Electronic Proceedings in Theoretical Computer Science (EPCS), vol 34, page 5 - 21, 2010. (electronic version of proceeding) (abstract) (pdf) (Implementation of type-checker in Haskell)
• Brigitte Pientka. Programming inductive proofs: a new approach based on contextual types, Brigitte Pientka, Verification, Induction, and Termination analysis, Lecture Notes in Artificial Intelligence (LNAI), Springer, 2010
• Brigitte Pientka. Beluga: programming with dependent types, contextual data, and contexts (Invited talk). In 10th International Symposium on Functional and Logic Programming (FLOPS'10), Lecture Notes in Computer Science (LNCS), vol 6009, page 1-12, Springer, 2010. (abstract) (pdf)
• Brigitte Pientka and Joshua Dunfield. Programming with proofs and explicit contexts. In ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'08), pages 163-173. ACM Press, July 2008. (abstract) (pdf) (bibtex)
• Joshua Dunfield and Brigitte Pientka. Case analysis of higher-order data. In International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08). Elsevier, June 2008. (abstract) (pdf—extended version including appendix) (bibtex)
• Brigitte Pientka. A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In 35th ACM Symposium on Principles of Programming Languages (POPL'08), pages 371-382. ACM Press, January 2008. (abstract) (pdf) (bibtex)