L773:1611 3349 OR L773:0302 9743
Search: L773:1611 3349 OR L773:0302 9743 > (2005-2009) > Formalized metatheo...
- 4 of 253
- Previous record
- Next record
- To hitlist
- Adams, Robin,1978Royal Holloway University of London (author)
Formalized metatheory with terms represented by an indexed family of types
- Article/chapterEnglish2006
Publisher, publication year, extent ...
- Berlin, Heidelberg :Springer Berlin Heidelberg,2006
- electronicrdacarrier
Numbers
- LIBRIS-ID:oai:research.chalmers.se:af4e16c3-abc8-4974-9bff-ec3aa56e8553
- https://research.chalmers.se/publication/504625URI
- https://doi.org/10.1007/11617990_1DOI
Supplementary language notes
- Language:English
- Summary in:English
Part of subdatabase
- SwePubSwePub
Classification
Notes
- 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.
Subject headings and genre
- 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
- type theory
- syntax with binding
- formalisation of mathematics
Added entries (persons, corporate bodies, meetings, titles ...)
- Royal Holloway University of London (creator_code:org_t)
Related titles
- In:Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)Berlin, Heidelberg : Springer Berlin Heidelberg3839, s. 1-161611-33490302-9743
Internet link
Find in a library
- Lecture Notes in Computer Science (including subseries Lecture Notes in Artifici... (Search for host publication in LIBRIS)
To the university's database
- 4 of 253
- Previous record
- Next record
- To hitlist
Find more in SwePub
- By the author/editor
- Adams, Robin, 19 ...
- About the subject
-
- NATURAL SCIENCES
- NATURAL SCIENCES
- and Mathematics
- and Algebra and Logi ...
-
- NATURAL SCIENCES
- NATURAL SCIENCES
- and Computer and Inf ...
- and Computer Science ...
- Articles in the publication
- Lecture Notes in ...
- By the university
- Chalmers University of Technology
Search outside SwePub
- Extend your search to:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - National Library Systems
- LIBRIS.kb.se
