Post-Proceedings of TYPES 2009 The Post-Proceedings of the TYPES 2009 Annual Workshop http://lama.univ-savoie.fr/types09/ will be published, after a formal referee process, as a volume of the Electronic Proceedings in Theoretical Computer Science (EPTCS) series http://eptcs.org/ . Submissions are not restricted to works presented at the workshop, nor are authors expected to be formally involved in the Types project. Deadlines - abstract submission: Wednesday, May 19th, 2010, 12:00 Paris time, - paper submission: Wednesday, May 26th, 2010, 12:00 Paris time. We encourage submissions on the themes of the Types Project http://www.cs.chalmers.se/Cs/Research/Logic/Types/ . The aim of Types 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. We invite submission of high quality papers, written in English and typeset in LaTeX2e using the EPTCS style: http://style.eptcs.org/ . Submissions should not have been published and should not be under consideration for publication elsewhere. We encourage authors to keep their submissions below 30 pages. Authors should submit their papers electronically to Tom Hirschowitz. The guest editors, Thorsten Altenkirch, Tom Hirshowitz, Christophe Raffalli, and Alan Schmitt. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]