CPSC 629: Deductive Systems
Instructor: Carsten Schürmann
Department of Computer Science
Yale University
Time: TTh 4:00-5:15
Room: AKW 500
|
|
Home |
|
|
Schedule |
|
|
Handouts |
|
|
Assignments |
|
|
Projects |
|
|
Links |
Lecture 9: Twelf
In this lecture we will see the Twelf system in action. Twelf is an implementation of the logical framework LF which supports the representation and specification of object languages such as Mini-ML, the implementation of algorithms such as Mini-ML's operational semantics, and the derivation of meta-theoretical properties, such as the value soundness or type preservation theorem.Suggested Reading Materials:
Frank Pfenning, Carsten Schürmann. Twelf User's Guide, Version 1.3.. Distributed with the Twelf system. Available from the Twelf homepage.
Frank Pfenning. Computation and Deduction, Chapter 4
Source Code:
Previous lecture: Lecture 8
Next lecture: Lecture 10