Tag Archives: types

Typechecking TAL0 in Agda.

This post is an annotated solution to problem 4.2.11 in the book Advanced Topics in Types and Programming Languages from the chapter Typed Assembly Language by Gerg Morrisett. Introducing TAL0 I’ll do my best to give an informal introduction to … Continue reading

Posted in Computers | Tagged , , , , , , | Leave a comment

[Proof] λ→ is normalizing

I studied a proof today that I had been putting off for some time now; that a simply typed lambda calculus is normalizing — every well-typed expression eventually reduces to a value. The proof is quite clever and that the … Continue reading

Posted in Computers, Rest | Tagged , , , | Leave a comment