APAL
2010
13 years 11 months ago
2010
A logic-enriched type theory (LTT) is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named LTT0 and LTT 0, which we...
CIE
2008
Springer
14 years 1 months ago
2008
Springer
Nested datatypes are families of datatypes that are indexed over all types and where the datatype constructors relate different members of the family. This may be used to represent...
TYPES
2000
Springer
14 years 3 months ago
2000
Springer
We present a formalization of the halting problem in Agda, a language based on Martin-L
BIRTHDAY
2006
Springer
14 years 3 months ago
2006
Springer
Abstract. This paper gives a reduction-preserving translation from Coquand's dependent pattern matching [4] into a traditional type theory [11] with universes, inductive types...
IMPERIAL
1993
14 years 3 months ago
1993
This work expounds the notion that (structured) categories are syntax free presentations of type theories, and shows some of the ideas involved in deriving categorical semantics f...
SIGSOFT
1996
ACM
14 years 3 months ago
1996
ACM
Abstract -- Software architectures enable large-scale software development. Component reuse and substitutability, two key aspects of large-scale development, must be planned for du...
CSL
1997
Springer
14 years 3 months ago
1997
Springer
Abstract. Milner introduced action calculi as a framework for investigating models of interactive behaviour. We present a type-theoretic account of action calculi using the proposi...
LICS
1999
IEEE
14 years 3 months ago
1999
IEEE
We present a new approach to introducing an extensional propositional equality in Intensional Type Theory. Our construction is based on the observation that there is a sound, inte...
CADE
2000
Springer
14 years 3 months ago
2000
Springer
We provide techniques to integrate resolution logic with equality in type theory. The results may be rendered as follows. − A clausification procedure in type theory, equipped w...
CSL
2001
Springer
14 years 4 months ago
2001
Springer
Abstract. In this paper we show how to extend a constructive type theory with a principle that captures the spirit of Markov’s principle from constructive recursive mathematics. ...