Sökning: L773:1611 3349 OR L773:0302 9743
> (2005-2009) >
Formalized metatheo...
Formalized metatheory with terms represented by an indexed family of types
-
- Adams, Robin, 1978 (författare)
- Royal Holloway University of London
-
(creator_code:org_t)
- Berlin, Heidelberg : Springer Berlin Heidelberg, 2006
- 2006
- Engelska.
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. ; 3839, s. 1-16
- Relaterad länk:
-
https://research.cha... (primary) (free)
-
visa fler...
-
https://research.cha...
-
https://research.cha...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- It is possible to represent the terms of a syntax with binding constructors by a family of types, indexed by the free variables that may occur. This approach has been used several times for the study of syntax and substitution, but never for the formalization of the metatheory of a typing system. We describe a recent formalization of the metatheory of Pure Type Systems in Coq as an example of such a formalization. In general, careful thought is required as to how each definition and theorem should be stated, usually in an unfamiliar ‘big-step’ form; but, once the correct form has been found, the proofs are very elegant and direct.
Ämnesord
- NATURVETENSKAP -- Matematik -- Algebra och logik (hsv//swe)
- NATURAL SCIENCES -- Mathematics -- Algebra and Logic (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- type theory
- syntax with binding
- formalisation of mathematics
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas