TY - BOOK
T1 - Types for Proofs and Programs
A2 - Callaghan, Paul
A2 - Luo, Zhaohui
A2 - McKinna, James
A2 - Pollack, Robert
PY - 2002
Y1 - 2002
N2 - This book contains a selection of papers presented at the first annual workshop of the TYPES Working Group (Computer-Assisted Reasoning Based on Type Theory, EU IST project 29001), which was held 8th – 12th of December, 2000 at the University of Durham, Durham, UK. It was attended by about 80 researchers.The workshop follows a series of meetings organised in 1993, 1994, 1995, 1996, 1998, and 1999 under the auspices of the Esprit BRA 6435 and the Esprit Working Group 21900 for the previous TYPES projects. Those proceedings were also published in the LNCS series, edited by Henk Barendregt and Tobias Nipkow (Vol. 806, 1993), by Peter Dybjer, Bengt Nordstr¨om, and Jan Smith (Vol. 996, 1994), by Stefano Berardi and Mario Coppo (Vol. 1158, 1995), by Christine Paulin-Mohring and Eduardo Gimenez (Vol. 1512, 1996), by Thorsten Altenkirch, Wolfgang Naraschewski, and Bernhard Reus (Vol. 1657, 1998), and by Thierry Coquand, Peter Dybjer, Bengt Nordstr¨om, and Jan Smith (Vol. 1956, 1999). The Esprit BRA 6453 was itself a continuation of the former Esprit Action 3245, Logical Frameworks: Design, Implementation, and Experiments. The articles from the annual workshops under that Action were edited by Gerard Huet and Gordon Plotkin in the books Logical Frameworks and Logical Environments, both published by Cambridge University Press.
AB - This book contains a selection of papers presented at the first annual workshop of the TYPES Working Group (Computer-Assisted Reasoning Based on Type Theory, EU IST project 29001), which was held 8th – 12th of December, 2000 at the University of Durham, Durham, UK. It was attended by about 80 researchers.The workshop follows a series of meetings organised in 1993, 1994, 1995, 1996, 1998, and 1999 under the auspices of the Esprit BRA 6435 and the Esprit Working Group 21900 for the previous TYPES projects. Those proceedings were also published in the LNCS series, edited by Henk Barendregt and Tobias Nipkow (Vol. 806, 1993), by Peter Dybjer, Bengt Nordstr¨om, and Jan Smith (Vol. 996, 1994), by Stefano Berardi and Mario Coppo (Vol. 1158, 1995), by Christine Paulin-Mohring and Eduardo Gimenez (Vol. 1512, 1996), by Thorsten Altenkirch, Wolfgang Naraschewski, and Bernhard Reus (Vol. 1657, 1998), and by Thierry Coquand, Peter Dybjer, Bengt Nordstr¨om, and Jan Smith (Vol. 1956, 1999). The Esprit BRA 6453 was itself a continuation of the former Esprit Action 3245, Logical Frameworks: Design, Implementation, and Experiments. The articles from the annual workshops under that Action were edited by Gerard Huet and Gordon Plotkin in the books Logical Frameworks and Logical Environments, both published by Cambridge University Press.
U2 - 10.1007/3-540-45842-5
DO - 10.1007/3-540-45842-5
M3 - Book
SN - 9783540432876
T3 - Lecture Notes in Computer Science
BT - Types for Proofs and Programs
PB - Springer
ER -