Wyniki wyszukiwania - BazTech

Ograniczanie wyników

4 Fundamenta Informaticae

Znaleziono wyników: 4

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

A Note on Forcing and Type Theory

Coquand T., Jaber G.

Fundamenta Informaticae

2010

Vol. 100, nr 1/4

43-52

The goal of this note is to show the uniform continuity of definable functional in intuitionistic type theory as an application of forcing with dependent type theory.

Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs

Abel A., Coquand T.

Fundamenta Informaticae

2007

Vol. 77, nr 4

345-395

Martin-Löf's Logical Framework is extended by strong S-types and presented via judgmental equality with rules for extensionality and surjective pairing. Soundness of the framework rules is proven via a generic PER model on untyped terms. An algorithmic version of the framework is given through an untyped bh-equality test and a bidirectional type checking algorithm. Completeness is proven by instantiating the PER model with h-equality on b-normal forms, which is shown equivalent to the algorithmic equality.

The Completeness of Typing for Context-Semantics

Coquand T.

Fundamenta Informaticae

2007

Vol. 77, nr 4

293-301

We present a variation of Hindley's completeness theorem for simply typed [lambda]-calculus. It is based on a Kripke semantics where the worlds are contexts, called context-semantics. This variation was obtained indirectly by simplifying an analysis of a fragment of polymorphic [lambda]-calculus [2]. We relate in this way works done in proof theory [4,14] with a fundamental result in [lambda]-calculus.

A Logical Framework with Dependently Typed Records

Coquand T., Pollack R., Takeyama M.

Fundamenta Informaticae

2005

Vol. 65, nr 1,2

113--134