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

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

Last update Fri May 25 08:43:37 2012 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page