Lecture 8: Datatypes cont'd.

Today we continue our discussion on datatypes. We embark on a strange endeavour. Can we implement a funcational language within itself. This will reveal plenty of interesting features of datatype system. In the second part of the lecture I will give a brief demo of the Twelf system.

Further Reading:

Code

Here are the two files if you want to follow the type preservation proof in Twelf: sources.cfg, lec8.elf

Previous lecture: Lecture 7
Next lecture: Lecture 9