Lecture Notes in Computer Science - Types for Proofs and Programs
Latest Publications

TOTAL DOCUMENTS

15

(FIVE YEARS 0)

H-INDEX

7

(FIVE YEARS 0)

Published By Springer Berlin Heidelberg

9783540432876, 9783540458425

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Generalization in Type Theory Based Proof Assistants

Lecture Notes in Computer Science - Types for Proofs and Programs ◽

10.1007/3-540-45842-5_14 ◽

2002 ◽

pp. 217-232 ◽

Author(s):

Olivier Pons

Keyword(s):

Type Theory ◽

Proof Assistants

Download Full-text

On the Proofs of Some Formally Unprovable Propositions and Prototype Proofs in Type Theory

Lecture Notes in Computer Science - Types for Proofs and Programs ◽

10.1007/3-540-45842-5_11 ◽

2002 ◽

pp. 160-180 ◽

Author(s):

Giuseppe Longo

Keyword(s):

Download Full-text

A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals

Lecture Notes in Computer Science - Types for Proofs and Programs ◽

10.1007/3-540-45842-5_7 ◽

2002 ◽

pp. 96-111 ◽

Author(s):

Herman Geuvers ◽

Freek Wiedijk ◽

Jan Zwanenburg

Keyword(s):

Fundamental Theorem ◽

Constructive Proof ◽

Fundamental Theorem Of Algebra

Download Full-text

A Tour with Constructive Real Numbers

Lecture Notes in Computer Science - Types for Proofs and Programs ◽

10.1007/3-540-45842-5_3 ◽

2002 ◽

pp. 41-52 ◽

Author(s):

Alberto Ciaffaglione ◽

Pietro Di Gianantonio

Keyword(s):

Download Full-text

Executing Higher Order Logic

Lecture Notes in Computer Science - Types for Proofs and Programs ◽

10.1007/3-540-45842-5_2 ◽

2002 ◽

pp. 24-40 ◽

Author(s):

Stefan Berghofer ◽

Tobias Nipkow

Keyword(s):

Higher Order ◽

Order Logic ◽

Higher Order Logic

Download Full-text

A Kripke-Style Model for the Admissibility of Structural Rules

Lecture Notes in Computer Science - Types for Proofs and Programs ◽

10.1007/3-540-45842-5_8 ◽

2002 ◽

pp. 112-124 ◽

Author(s):

Healfdene Goguen

Keyword(s):

Structural Rules

Download Full-text

An Implementation of Type:Type

Lecture Notes in Computer Science - Types for Proofs and Programs ◽

10.1007/3-540-45842-5_4 ◽

2002 ◽

pp. 53-62

Author(s):

Thierry Coquand ◽

Makoto Takeyama

Download Full-text

Collection Principles in Dependent Type Theory

Lecture Notes in Computer Science - Types for Proofs and Programs ◽

10.1007/3-540-45842-5_1 ◽

2002 ◽

pp. 1-23 ◽

Author(s):

Peter Aczel ◽

Nicola Gambino

Keyword(s):

Type Theory ◽

Dependent Type Theory ◽

Download Full-text

Changing Data Structures in Type Theory: A Study of Natural Numbers

Lecture Notes in Computer Science - Types for Proofs and Programs ◽

10.1007/3-540-45842-5_12 ◽

2002 ◽

pp. 181-196 ◽

Author(s):

Nicolas Magaud ◽

Yves Bertot

Keyword(s):

Data Structures ◽

Type Theory ◽

Natural Numbers

Download Full-text

Towards Limit Computable Mathematics

Lecture Notes in Computer Science - Types for Proofs and Programs ◽

10.1007/3-540-45842-5_9 ◽

2002 ◽

pp. 125-144 ◽

Author(s):

Susumu Hayashi ◽

Masahiro Nakata

Download Full-text