Skip to content

Instantly share code, notes, and snippets.

@osa1
Last active January 3, 2016 10:39
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 1 You must be signed in to fork a gist
  • Save osa1/f34ec1101e65b490e3b6 to your computer and use it in GitHub Desktop.
Save osa1/f34ec1101e65b490e3b6 to your computer and use it in GitHub Desktop.

BIL496 Project Abstract

Mechanizing Metatheory of Multi-stage Lambda Calculus

Giving mechanized metatheory of languages in theorem provers has been an interest for programming language researchers for a while now. Some of them even dream of providing mechanized proofs together with scientific papers, instead of additional technical report papers.

Mechanized proofs are carried out in an interactive theorem prover. Interactive theorem provers rely on a constructive type theory to have consistent logic 1 that allows proofs to be given in. In these theorem provers, theorems are represented as types and proofs are represented as programs 2, meaning that one actually proves theorems by writing programs 3. In our case, we will be using the Coq interactive theorem prover, which is very popular amongst programming language researchers. During the project we expect to frequently refer to a book that teaches programming language theory using Coq: Software Foundations 4.

Main goal of this project is to provide Coq implementation of multi-staged lambda calculus, as described in Choi et al. 5. The paper also provides theory about translating a multi-staged language into a non-staged one, running some static analysis on translated language, and then translating it back to staged language, while preserving the semantics and mapping analysis results to staged language. Depending on how well we do on first part, we also want to work on this part.

Main contribution of this project will be providing an implementation of a typed, multi-staged lambda calculus and it's proofs in an interactive theorem prover. Most importantly, we want to give type soundness proof (and for this we need to show progress and preservation properties) of multi-staged language with open code 6.


Footnotes

  1. One of my aims while doing this project is also explore this area more.

  2. "Types-as-propositions, programs-as-proof" is a well-known relationship between types and programs, called "Curry-Howard isomorphism".

  3. That part is not always obvious, though. This is because some theorem provers provide additional languages to generate proof programs. So users actually write in another language which is generally more similar to the language used in proofs in mathematics. Programs are later generated from user programs written in that higher-level language. This is also the case with Coq.

  4. http://www.cis.upenn.edu/~bcpierce/sf/

  5. Wontae Choi, Baris Aktemur, Kwangkeun Yi, and Makoto Tatsuta. 2011. Static analysis of multi-staged programs via unstaging translation. SIGPLAN Not. 46, 1 (January 2011), 81-92. DOI=10.1145/1925844.1926397 http://doi.acm.org/10.1145/1925844.1926397

  6. In this context, open code means having free (unbound) variables in staged code.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment