University of Cambridge > > Mini Courses in Theoretical Computer Science > Mechanizing Theories in Twelf: A Tutorial (Part 2)

Mechanizing Theories in Twelf: A Tutorial (Part 2)

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Sam Staton.

As researchers in theory, and in particular, programming language theory, we are interested in theorems and proofs. For high-assurance, we want these to be checkable automatically. Various proof assistants have been devised and used for mechanizing some realistic proofs, as well as challenges such as POP Lmark. The Twelf tool is such a proof assistant, with support for representation of formal systems and inductive proofs over them. It supports and encourages a method of representation known as higher-order abstract syntax, which simplifies reasoning about systems with binding structures and with hypothetical reasoning.

This course is a tutorial introduction to Twelf, in its role as a system for representing formal systems and checking proofs about them. We will look at encodings of systems, proofs about them, and helpful strategies to convince Twelf we have a good proof. We will also learn how to understand a proof we get, and believe in these proofs. Our examples will be drawn from the metatheory of programming languages and type systems.

Course materials will be put here .

This talk is part of the Mini Courses in Theoretical Computer Science series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity