


default search action
TYPES 1996: Aussois, France
- Eduardo Giménez, Christine Paulin-Mohring:

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 - 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 A. 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

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














