Computation and Logic Group, McGill University, May 2013-August 2014.
Today, we routinely specify and reason about the runtime behaviour of software using formal systems such as type systems or logics for access control to establish safety properties. In our work, we concentrate on Beluga, a novel programming and proof environment which supports specifying formal systems in the logical framework LF via axioms and inference rules. It provides direct support for common and tricky routines dealing with variables, such as capture-avoiding substitution and renaming. Moreover, Beluga allows embedding contextual LF objects, i.e. a LF object together with the context in which it is meaningful, in programs.
Our work provides a foundation for writing total functions over contextual objects. More broadly, it provides an important, currently missing piece in the foundation of the proof and programming language Beluga since it justifies that well-founded recursive programs implement well-founded inductive proofs. The work has a wide range of implications and applications in certified programming, proof-carrying architectures, and mechanizing meta-theory of programming languages.
- Brigitte Pientka, Sherry Shanshan Ruan, Andreas Abel. Structural Recursion over Contextual Objects. [Long version]
- Structural Recursion over Contextual Objects. The 19th ACM SIGPLAN International Conference on Functional Programming (ICFP’14), Gothenburg, Sweden, September 1-3, 2014. [Abstract] [Poster] [Slides]
- Well-founded Recursion over Contextual Objects. Opportunities for Undergraduate Research in Computer Science Workshop (OurCS’13), Carnegie Mellon University, Pittsburgh, PA, United States, October 18-20, 2013. [Poster]
- Well-founded Recursion over Contextual Objects. Selected to represent mathematical and computational sciences at the 9th McGill Annual Undergraduate Research Conference (URC’13), Montreal, QC, Canada, October 10, 2013. [Poster] [Slides]
- See the Beluga project page for a detailed description of the project and other resources