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

TOTAL DOCUMENTS

(FIVE YEARS 0)

H-INDEX

(FIVE YEARS 0)

Published By Springer Berlin Heidelberg

9783540617808, 9783540707226

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Conservativity of equality reflection over intensional type theory

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

10.1007/3-540-61780-9_68 ◽

1996 ◽

pp. 153-164 ◽

Cited By ~ 6

Author(s):

Martin Hofmann

Keyword(s):

Type Theory

Download Full-text

Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids

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

10.1007/3-540-61780-9_61 ◽

1996 ◽

pp. 47-61 ◽

Cited By ~ 7

Author(s):

Ilya Beylin ◽

Peter Dybjer

Keyword(s):

Monoidal Categories

Download Full-text

An algorithm for checking incomplete proof objects in type theory with localization and unification

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

10.1007/3-540-61780-9_70 ◽

1996 ◽

pp. 183-200

Author(s):

Lena Magnusson

Keyword(s):

Type Theory

Download Full-text

A simple model construction for the Calculus of Constructions

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

10.1007/3-540-61780-9_74 ◽

1996 ◽

pp. 249-264 ◽

Cited By ~ 6

Author(s):

M. Stefanova ◽

H. Geuvers

Keyword(s):

Simple Model ◽

Model Construction ◽

Calculus Of Constructions

Download Full-text

An application of constructive completeness

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

10.1007/3-540-61780-9_63 ◽

1996 ◽

pp. 76-84

Author(s):

Thierry Coquand ◽

Jan M. Smith

Download Full-text

Circuits as streams in Coq: Verification of a sequential multiplier

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

10.1007/3-540-61780-9_72 ◽

1996 ◽

pp. 216-230 ◽

Cited By ~ 10

Author(s):

Christine Paulin-Mohring

Download Full-text

Optimized encodings of fragments of type theory in first order logic

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

10.1007/3-540-61780-9_75 ◽

1996 ◽

pp. 265-287 ◽

Cited By ~ 1

Author(s):

Tanel Tammet ◽

Jan M. Smith

Keyword(s):

Type Theory ◽

Order Logic ◽

First Order Logic ◽

First Order

Download Full-text

Automating inversion of inductive predicates in Coq

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

10.1007/3-540-61780-9_64 ◽

1996 ◽

pp. 85-104 ◽

Cited By ~ 9

Author(s):

Cristina Cornes ◽

Delphine Terrasse

Download Full-text

An application of co-inductive types in Coq: Verification of the alternating bit protocol

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

10.1007/3-540-61780-9_67 ◽

1996 ◽

pp. 135-152 ◽

Cited By ~ 17

Author(s):

Eduardo Giménez

Keyword(s):

Alternating Bit Protocol ◽

Inductive Types

Download Full-text

Context-relative syntactic categories and the formalization of mathematical text

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

10.1007/3-540-61780-9_73 ◽

1996 ◽

pp. 231-248 ◽

Cited By ~ 2

Author(s):

Aarne Ranta

Keyword(s):

Mathematical Text

Download Full-text

Lecture Notes in Computer Science - Types for Proofs and ProgramsLatest Publications

TOTAL DOCUMENTS

H-INDEX

Published By Springer Berlin Heidelberg

Conservativity of equality reflection over intensional type theory

Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids

An algorithm for checking incomplete proof objects in type theory with localization and unification

A simple model construction for the Calculus of Constructions

An application of constructive completeness

Circuits as streams in Coq: Verification of a sequential multiplier

Optimized encodings of fragments of type theory in first order logic

Automating inversion of inductive predicates in Coq

An application of co-inductive types in Coq: Verification of the alternating bit protocol

Context-relative syntactic categories and the formalization of mathematical text

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