TYPES 1996: Aussois, France

Eduardo Giménez, Christine Paulin-Mohring (Eds.): Types for Proofs and Programs, International Workshop TYPES'96, Aussois, France, December 15-19, 1996, Selected Papers. Lecture Notes in Computer Science 1512 Springer 1998, ISBN 3-540-65137-3 BibTeX

@proceedings{DBLP:conf/types/1996,
  editor    = {Eduardo Gim{\'e}nez and
               Christine Paulin-Mohring},
  title     = {Types for Proofs and Programs, International Workshop TYPES'96,
               Aussois, France, December 15-19, 1996, Selected Papers},
  booktitle = {TYPES},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1512},
  year      = {1998},
  isbn      = {3-540-65137-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Eduardo Giménez, Christine Paulin-Mohring: Introduction. 1-8 BibTeX
Anthony Bailey: Coercion Synthesis in Computer Implementations of Type-Theoretic Frameworks. 9-27 BibTeX
Bruno Barras: Verification of the Interface of a Small Proof System in Coq. 28-45 BibTeX
Jan Cederquist: An Implementation of the Heine-Borel Covering Theorem in Type Theory. 46-65 BibTeX
Ferruccio Damiani, Frédéric Prost: Detecting and Removing Dead-Code using Rank 2 Intersection. 66-87 BibTeX
Gilles Dowek: A Type-Free Formalization of Mathematics where Proofs are Objects. 88-111 BibTeX
Daniel Fridlender: Highman's Lemma in theory. 112-133 BibTeX
Jean Goubault-Larrecq: A Proof of Weak Termination of Typed lambda-sigma-Calculi. 134-153 BibTeX
John Harrison: Proof Style. 154-172 BibTeX
Alex P. Jones, Zhaohui Luo, Sergei Soloviev: Some Algorithmic and Proof-Theoretical Aspects of Coercive Subtyping. 173-195 BibTeX
Petri Mäenpää: Semantical BNF. 196-215 BibTeX
Maria Emilia Maietti: The Internal Type Theory of a Heyting Pretopos. 216-235 BibTeX
Conor McBride: Inverting Inductively Defined Relations in LEGO. 236-253 BibTeX
Paul-André Melliès, Benjamin Werner: A Generic Normalisation Proof for Pure Type Systems. 254-276 BibTeX
Jean-François Monin: Proving a Real Time Algorithm for ATM in Coq. 277-293 BibTeX
César Muñoz: Dependent Types with Explicit Substitutiuons: A Meta-theoretical development. 294-316 BibTeX
Wolfgang Naraschewski, Tobias Nipkow: Type Inference Verified: Algorithm W in Isabelle/HOL. 317-332 BibTeX
Sara Negri: Continous Lattices in Formal Topology. 333-353 BibTeX
Alvaro Tasistro: Abstract Insertion Sort in an Extension of Type Theory with Record Types and Subtyping. 354-372 BibTeX