Changes between Version 21 and Version 22 of WikiStart

Timestamp:

Dec 31, 2012, 9:47:58 PM (11 years ago)

Author:

benl

Comment:

--

WikiStart

@@ -1 +1 @@
 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.
 
-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.]
+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.