The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

Thorsten wrote:
> The lego code is at http://www.cs.nott.ac.uk/~txa/publ/tlca93.zip
> (this includes the proof for simply typed lambda calculus).
> I don't think lego is still working :-(

Thanks to James McKinna it is possible to run LEGO on modern Linux.
Contact James for info.

Randy
--
On Tue, May 13, 2014 at 10:49 AM, Altenkirch Thorsten
<psztxa AT exmail.nottingham.ac.uk>
 wrote:
> Hi Kazuhiko,
>
> my old proof '93 in LEGO (in pure CC + handcoded inductive types using
> only eliminators) I needed 1647 lines. :-)
>
> @InProceedings{alti:tlca93,
>   author =      "Thorsten Altenkirch",
>   title =       "A Formalization of the Strong Normalization Proof for
> {System F} in {LEGO}",
>   booktitle =   "Typed Lambda Calculi and Applications",
>   year =        "1993",
>   editor =      "M. Bezem, J.F. Groote",
>   series =      "LNCS 664",
>   pages =       "13 - 28",
> }
>
>
> The lego code is at http://www.cs.nott.ac.uk/~txa/publ/tlca93.zip
> (this includes the proof for simply typed lambda calculus).
> I don't think lego is still working :-(
>
> Chhers,
> Thorsten
>
> On 13/05/2014 07:41, "Kazuhiko Sakaguchi" 
> <s1111365 AT coins.tsukuba.ac.jp>
> wrote:
>
>>Dear all,
>>
>>I have formalized the strong normalization theorem of the System F in
>>SSReflect.
>>The formalization is available at:
>>https://github.com/pi8027/lambda-calculus/blob/master/coq/LC/Debruijn/F.v
>>
>>I assembled the proofs into a file (1,166 lines, 42KB).
>>Does anybody know of a shorter formalization?
>>https://gist.github.com/pi8027/9640431
>>
>>Regards,
>>Kazuhiko Sakaguchi
>
> This message and any attachment are intended solely for the addressee and 
> may contain confidential information. If you have received this message in 
> error, please send it back to me, and immediately delete it.   Please do 
> not use, copy or disclose the information contained in this message or in 
> any attachment.  Any views or opinions expressed by the author of this 
> email do not necessarily reflect the views of the University of Nottingham.
>
> This message has been checked for viruses but the contents of an attachment
> may still contain software viruses which could damage your computer system, 
> you are advised to perform your own checks. Email communications with the 
> University of Nottingham may be monitored as permitted by UK legislation.
>
>
>
>
>