TaPL.lean

Implementing and learning Types and Programming Languages in Lean 3

This code does not have one-to-one correspondence to the original implentation

Run

lean --run src/main.lean LANGUAGE_NAME at project root

Progress

• Chapter 1~4
  • arith
• Chapter 5~7
  • untyped
  • fulluntyped
• Chapter 8
  • tyarith
• Chapte 9~10
  • simplebool
  • fullsimple
• bot
• equirec
• fomega
• fomsub
• fullequirec
• fullerror
• fullfomsub
• fullfsub
• fullisorec
• fullomega
• fullpoly
• fullrecon
• fullref
• fullsub
• fullupdate
• letexercise
• purefsub
• rcdsubbot
• recon
• reconbase

License

The test.f file in each directories under examples is copied from the original implentation, and their copyright belongs to Benjamin C. Pierce as far as I know (I couldn't find the copyright notice of them).

Everything else (including examples/#/test_ex.f) is licensed under the BSD3 License - see the LICENSE.txt file for details