Extended calculus of constructions as a specification language

0Citations
Citations of this article
1Readers
Mendeley users who have this article in their library.
Get full text

Abstract

Huet and Coquand’s Calculus of Constructions, an implementation of type theory, was extended by Luo with sigma types, a type of pairs where the type of the second component depends on the value of the first one. This calculus has been implemented as ‘Lego’ by Pollack. The system and documentation is obtainable thus: ftp ftp.dcs.ed.ac.uk cd export/lego, after which one should read the file README. The sigma types enable one to give a compact description of abstract mathematical structures such as ‘group’, to build more concrete structures of them, such as ‘the group of integers under addition’ and to check that the concrete structure is indeed an instance of the abstract one. The trick is that the concrete structure includes as components proofs that it satisfies the axioms of the abstract structures. So ‘group’ is a sigma type and ‘group of integers under addition’ is an n-tuple of types, operators and proofs which is an element of this sigmatype. We can define functions which enrich such structures or forget them to simpler ones. However the calculus is intentional and it is too restrictive to identify the mathematical notion of ‘set’ with ‘type’. We will discuss how sets and functions between them may be represented and the notational difficulties which arise. We put forward a tentative suggestion as to how these difficulties might be overcome by defining the category of sets and functions in the calculus, then using the internal language of that category to extend the type theory. This would be a particular example of a more general reflection principle.

Cite

CITATION STYLE

APA

Burstall, R. (1993). Extended calculus of constructions as a specification language. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 669 LNCS). Springer Verlag. https://doi.org/10.1007/3-540-56625-2_1

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free