Changes between Version 12 and Version 13 of WikiStart

Timestamp:

Dec 27, 2012, 3:06:26 PM (12 years ago)

Author:

benl

Comment:

--

WikiStart

@@ -1 +1 @@
 = Iron Lambda =
 
-Iron Lambda is a collection of Coq formalisations for functional languages of increasing complexity. The aim of the project is to get the proofs done and not worry too much about using the coolest new approaches. 
+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.
 
-All proofs use straight deBruijn indices for binders, which are fairly usable once you understand what lifting lemmas are required. They 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 tricky LTac code to make it smaller.
+As the focus of Iron Lambda is more on programming language semantics than the coolest new proving techniques, 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 tricky LTac code to make it smaller.
 
 Style guidelines: