Published: 16th March 2011
DOI: 10.4204/EPTCS.53
ISSN: 2075-2180

EPTCS 53

Proceedings
Types for Proofs and Programs, Revised Selected Papers
Aussois, France, 12-15th May 2009

Edited by: Tom Hirschowitz
Preface
Superposition as a logical glue
Andrea Asperti and Enrico Tassi		1
Nonuniform Coercions via Unification Hints
Claudio Sacerdoti Coen and Enrico Tassi		16
Typed Operational Semantics for Dependent Record Types
Yangyue Feng and Zhaohui Luo		30
Stateless HOL
Freek Wiedijk		47

Preface

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ł Urzyczyn for excellent talks. The present volume consists of papers not necessarily presented at the workshop, selected by
with help from Matthieu Sozeau and Makarius Wenzel.