Proceedings Types for Proofs and Programs, Revised Selected Papers

TL;DR

This collection of papers from the Types for Proofs and Programs conference advances formal reasoning and programming languages based on Type Theory, with applications in software certification, mathematical formalisation, and language analysis.

Contribution

It presents new research and developments in type theory, formal reasoning tools, and their applications across programming languages and mathematics.

Findings

Enhanced type systems for formal verification

Development of tools for proof assistance

Applications in certified software and mathematical formalisation

Abstract

Types for Proofs and Programs is the annual meeting of the Types Project, whose aim is to develop the technology of formal reasoning and computer programming based on Type Theory. This is done by improving the languages and computerised tools for reasoning, and by applying the technology in several domains such as analysis of programming languages, certified software, formalisation of mathematics and mathematics education. The 2009 meeting took place in Aussois, France, and we thank the invited speakers Richard Garner, Peter Hancock, Pawe{\l} Urzyczyn for excellent talks. The present volume consists of papers not necessarily presented at the workshop, selected by Thorsten Altenkirch, Tom Hirschowitz, Christophe Raffalli, and Alan Schmitt, with help from Matthieu Sozeau and Makarius Wenzel.