Tools

LEADER 03132cam 2200373 a 4500

001 ocm35397905;

003 OCoLC;

005 20141212123100.0;

008 960830s1996 gw a b 001 0 eng ;

010 a| 96043300;

020 a| 3540617809 (alk. paper);

035 a| (Sirsi) o35397905;

035 a| (OCoLC)35397905;

049 a| EREE;

050 00 a| QA76.9.A96b| T96 1995;

082 00 a| 511.3/02852| 20;

111 2 a| TYPES '95d| (1995 :c| Turin, Italy)=| ^A384708;

245 10 a| Types for proofs and programs :b| international workshop TYPES '95, Torino, Italy, June 5-8, 1995 : selected papers /c| Stefano Berardi, Mario Coppo, (eds.).;

300 a| x, 296 pages :b| illustrations ;c| 24 cm.;

336 a| text2| rdacontent;

337 a| unmediated2| rdamedia;

338 a| volume2| rdacarrier;

490 1 a| Lecture notes in computer science ;v| 1158;

504 a| Includes bibliographical references.;

505 0 a| Implicit coercions in type systems / Gilles Barthe -- A two-level approach towards lean proof-checking / Gilles Barthe, Mark Ruys and Henk Barendregt -- The greatest common divisor : a case study for program extraction from classical proofs / Ulrich Berger and Helmut Schwichtenberg -- Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids / Ilya Beylin and Peter Dybjer -- A constructive proof of the Heine-Borel covering theorem for formal reals / Jan Cederquist and Sara Negri -- An application of constructive completeness / Thierry Coquand and Jan Smith --Automating inversion of inductive predicates in Coq / Cristina Cornes and Delphine Terrasse -- First order marked types / Philippe Curmin -- Internal type theory / Peter Dybjer -- An application of co-inductive types in Coq : verification of the alternating bit protocol / Eduardo Giménez -- Conservativity of equality reflection over intensional type theory / Martin Hofmann -- A natural deduction approach to dynamic logic / Furio Honsell and Marino Miculan -- An algorithm for checking incomplete proof objects in type theory with localization and unification / Lena Magnusson -- Decidability of all minimal models / Vincent Padovani -- Circuits as streams in Coq : verification of a sequential multiplier / Christine Paulin-Mohring -- Context-relative syntactic categories and the formalization of mathematical text / Aarne Ranta -- A simple model construction for the calculus of constructions / Milena Stefanova and Herman Geuvers -- Optimized encodings of fragments of type theory in first order logic / Tanel Tammet and Jan Smith -- Organization and development of a constructive axiomatization / Jan von Plato.;

650 0 a| Automatic theorem provingv| Congresses.=| ^A24746;

700 1 a| Berardi, Stefano.=| ^A384709;

700 1 a| Coppo, Mario.=| ^A384710;

830 0 a| Lecture notes in computer sciencev| 1158.=| ^A466336;

596 a| 1;

998 a| 608475;

999 a| QA76.9.A96 T96 1995w| LCc| 1i| 30372009855765d| 3/6/2013f| 3/6/2013g| 1l| JGESm| JOYNERr| Ys| Yt| JGESBKu| 2/10/1997x| BOOKz| JSTACKSo| .STAFF. 0;

Types for proofs and programs : international workshop TYPES '95, Torino, Italy, June 5-8, 1995 : selected papers / Stefano Berardi, Mario Coppo, (eds.).

Author/creator	TYPES '95
Other author	Berardi, Stefano.
Other author	Coppo, Mario.
Format	Book
Publication Info	Berlin ; New York : Springer, ©1996.
Description	x, 296 pages : illustrations ; 24 cm.
Subjects	Automatic theorem proving--Congresses.

Series	Lecture notes in computer science ; 1158 Lecture notes in computer science 1158. ^A466336
Contents	Implicit coercions in type systems / Gilles Barthe -- A two-level approach towards lean proof-checking / Gilles Barthe, Mark Ruys and Henk Barendregt -- The greatest common divisor : a case study for program extraction from classical proofs / Ulrich Berger and Helmut Schwichtenberg -- Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids / Ilya Beylin and Peter Dybjer -- A constructive proof of the Heine-Borel covering theorem for formal reals / Jan Cederquist and Sara Negri -- An application of constructive completeness / Thierry Coquand and Jan Smith --Automating inversion of inductive predicates in Coq / Cristina Cornes and Delphine Terrasse -- First order marked types / Philippe Curmin -- Internal type theory / Peter Dybjer -- An application of co-inductive types in Coq : verification of the alternating bit protocol / Eduardo Giménez -- Conservativity of equality reflection over intensional type theory / Martin Hofmann -- A natural deduction approach to dynamic logic / Furio Honsell and Marino Miculan -- An algorithm for checking incomplete proof objects in type theory with localization and unification / Lena Magnusson -- Decidability of all minimal models / Vincent Padovani -- Circuits as streams in Coq : verification of a sequential multiplier / Christine Paulin-Mohring -- Context-relative syntactic categories and the formalization of mathematical text / Aarne Ranta -- A simple model construction for the calculus of constructions / Milena Stefanova and Herman Geuvers -- Optimized encodings of fragments of type theory in first order logic / Tanel Tammet and Jan Smith -- Organization and development of a constructive axiomatization / Jan von Plato.
Bibliography note	Includes bibliographical references.
LCCN	96043300
ISBN	3540617809 (alk. paper)

Types for proofs and programs : international workshop TYPES '95, Torino, Italy, June 5-8, 1995 : selected papers / Stefano Berardi, Mario Coppo, (eds.).

Click here for more information about this title