Iron Lambda is a collection of [http://coq.inria.fr Coq] formalisations for functional languages of increasing complexity. It fills part of the gap between the end of the [http://www.cis.upenn.edu/~bcpierce/sf/ Software Foundations] course and what appears in current research papers. If you are new to Coq then you would be better off starting with Software Foundations rather than this work.
We just use straight deBruijn indices for binders. Using deBruijn indices does require that we prove some lemmas about lifting and substitution, but they are very similar between languages, so the initial effort can be re-used. For more details see the blog post [http://disciple-devel.blogspot.com.au/2011/08/how-i-learned-to-stop-worrying-and-love.html How I learned to stop worrying and love deBruijn indices.]
The proofs use a "semi-[http://adam.chlipala.net/cpdt/ Chilpala]" approach to mechanisation: most lemmas are added to the global hint and rewrite databases, but if the proof script of a particular lemma was already of a sane length, then we haven't invested time writing lemma-specific LTac code to make it smaller.
Style guidelines:
* Verbose comments explaining what the main definitions and theorems
are for. The scripts should be digestable by intermediate Coq users.
* No unicode or infix operators for judgement forms.
When ''I'' use them in ''my'' proofs they make perfect sense, but when you
use them in yours they're completely unreadable.
* Heavy use of the `burn` megatactic. This is in the same vein as Chilpala's
`crush` tactic, but at the time I couldn't work out what `crush` was doing...
* Uses the `Case` and `SCase` etc tactics to add structure.
== Installation ==
* You will need a working version of [http://coq.inria.fr Coq]. The proofs are known to work with Coq 8.4.
* Source code is on github
{{{
git clone https://github.com/benl23x5/iron
}}}
* There is a top-level Makefile that will build all the proofs. For this to work `coqc` and `coqdep` need to be in your default path.
{{{
$ cd iron
$ make
}}}
* Each Coq module should check in under two minutes. If not then the automation might have diverged, so please tell me about it. Also report any build problems.
== More Information ==
* Send email to [http://www.cse.unsw.edu.au/~benl/ Ben Lippmeier] ``
* Read the [http://disciple-devel.blogspot.com.au/ Disciple Development] blog.
== Related Work ==
* [http://www.cis.upenn.edu/~bcpierce/sf/ Software Foundations]
* [http://adam.chlipala.net/cpdt/ Certified Programming with Dependent Types]
* [http://www.cis.upenn.edu/~bcpierce/papers/binders.pdf Engineering Formal Metatheory (paper)] [http://www.chargueraud.org/softs/ln/ (proofs)]
* [http://www.seas.upenn.edu/~plclub/poplmark/ The POPLmark Challenge]
* [http://compcert.inria.fr/ CompCert]
* [http://coq.inria.fr/cocorico/List%20of%20Coq%20PL%20Projects List of Programming Languages Coq projects]
[[br]]
[[br]]
= Current Languages =
Click the headings to get to the proofs.[[br]]
== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/Simple/ Simple] ==
Simply Typed Lambda Calculus (STLC).
"Simple" here refers to the lack of polymorphism.
== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SimplePCF/ SimplePCF] ==
STLC with booleans, naturals and fixpoint.
== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SimpleRef/ SimpleRef] ==
STLC with mutable references.
The typing judgement includes a store typing.
== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SimpleData/ SimpleData] ==
STLC with algebraic data and case expressions.
The definition of expressions uses indirect mutual recursion. Expressions contain a list of case-alternatives, and alternatives contain expressions, but the definition of the list type is not part of the same recursive group. The proof requires that we define our own induction scheme for expressions.
== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SystemF/ SystemF] ==
Compared to STLC, the proof for SystemF needs more lifting lemmas so it can deal with deBruijn indices at the type level.
== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SystemF2/ SystemF2] ==
Very similar to SystemF, but with higher kinds.
== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SystemF2Data/ SystemF2Data] ==
SystemF2 with algebraic data and case expressions.
Requires that we define simultaneous substitutions, which are used when subsituting expressions bound by pattern variables into the body of an alternative. The language allows data constructors to be applied to general expressions rather than just values, which requires more work when defining evaluation contexts.
== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SystemF2Store/ SystemF2Store] ==
SystemF2 with algebraic data, case expressions and a mutable store.
All data is allocated into the store and can be updated with primitive
polymorphic update operators.
== [https://github.com/benl23x5/iron/tree/master/done/Iron/Language/SystemF2Effect/ SystemF2Effect] ==
SystemF2 with a region and effect system. Supports region extension and deallocation.