Mechanizing Theories in Twelf: A Tutorial (Part 1)

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

• Susmit Sarkar
• Tuesday 27 February 2007, 10:00-12:00
• Computer Laboratory, Room FW11.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• All transferable skills in the university: computing
• Cambridge talks
• Computer Laboratory, Room FW11
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Mini Courses in Theoretical Computer Science
• Modelling Biology
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.