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

9783540605799, 9783540477709

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

The metatheory of UTT

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

10.1007/3-540-60579-7_4 ◽

1995 ◽

pp. 60-82 ◽

Cited By ~ 2

Author(s):

Healfdene Goguen

Download Full-text

On extensibility of proof checkers

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

10.1007/3-540-60579-7_8 ◽

1995 ◽

pp. 140-161 ◽

Cited By ~ 6

Author(s):

Robert Pollack

Download Full-text

I/O automata in Isabelle/HOL

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

10.1007/3-540-60579-7_6 ◽

1995 ◽

pp. 101-119 ◽

Cited By ~ 15

Author(s):

Tobias Nipkow ◽

Konrad Slind

Download Full-text

Formalization of a λ-calculus with explicit substitutions in Coq

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

10.1007/3-540-60579-7_10 ◽

1995 ◽

pp. 183-202 ◽

Cited By ~ 2

Author(s):

Amokrane Saïbi

Keyword(s):

Explicit Substitutions

Download Full-text

Communicating contexts: A pragmatic approach to information exchange

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

10.1007/3-540-60579-7_1 ◽

1995 ◽

pp. 1-13 ◽

Cited By ~ 1

Author(s):

René Ahn

Keyword(s):

Information Exchange ◽

Pragmatic Approach

Download Full-text

Syntactic categories in the language of mathematics

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

10.1007/3-540-60579-7_9 ◽

1995 ◽

pp. 162-182 ◽

Cited By ~ 3

Author(s):

Aarne Ranta

Download Full-text

Codifying guarded definitions with recursive schemes

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

10.1007/3-540-60579-7_3 ◽

1995 ◽

pp. 39-59 ◽

Cited By ~ 48

Author(s):

Eduarde Giménez

Download Full-text

A short and flexible proof of strong normalization for the calculus of constructions

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

10.1007/3-540-60579-7_2 ◽

1995 ◽

pp. 14-38 ◽

Cited By ~ 18

Author(s):

Herman Geuvers

Keyword(s):

Strong Normalization ◽

Calculus Of Constructions

Download Full-text

A user's friendly syntax to define recursive functions as typed λ-terms

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

10.1007/3-540-60579-7_5 ◽

1995 ◽

pp. 83-100 ◽

Cited By ~ 4

Author(s):

Pascal Manoury

Keyword(s):

Recursive Functions

Download Full-text

A concrete final coalgebra theorem for ZF set theory

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

10.1007/3-540-60579-7_7 ◽

1995 ◽

pp. 120-139 ◽

Cited By ~ 3

Author(s):

Lawrence C. Paulson

Keyword(s):

Set Theory

Download Full-text

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

TOTAL DOCUMENTS

H-INDEX

Published By Springer Berlin Heidelberg

The metatheory of UTT

On extensibility of proof checkers

I/O automata in Isabelle/HOL

Formalization of a λ-calculus with explicit substitutions in Coq

Communicating contexts: A pragmatic approach to information exchange

Syntactic categories in the language of mathematics

Codifying guarded definitions with recursive schemes

A short and flexible proof of strong normalization for the calculus of constructions

A user's friendly syntax to define recursive functions as typed λ-terms

A concrete final coalgebra theorem for ZF set theory

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