(WFRF:(Thierry B.)) srt2:(2015-2019)
Search: (WFRF:(Thierry B.)) srt2:(2015-2019) > (2015) > A generalization of...
- 1 of 1
- Previous record
- Next record
- To hitlist
A generalization of the Takeuti-Gandy interpretation
- Barras, B. (author)
-
- Coquand, Thierry, 1961 (author)
- Gothenburg University,Göteborgs universitet,Institutionen för data- och informationsteknik (GU),Department of Computer Science and Engineering (GU),University of Gothenburg
-
- Huber, Simon, 1984 (author)
- Gothenburg University,Göteborgs universitet,Institutionen för data- och informationsteknik, datavetenskap, programmeringslogik (GU),Department of Computer Science and Engineering, Computing Science, Programming Logic,University of Gothenburg
- (creator_code:org_t)
- 2015-02-20
- 2015
- English.
- In: Mathematical Structures in Computer Science. - : Cambridge University Press (CUP). - 0960-1295 .- 1469-8072. ; 25:5, s. 1071-1099
- Journal article (peer-reviewed)
Abstract
Subject headings
Close
- We present an interpretation of a version of dependent type theory where a type is interpreted by a Kan semisimplicial set. This interprets only a weak notion of conversion similar to the one used in the first published version of Martin-Lof type theory. Each truncated version of this model can be carried out internally in dependent type theory, and we have formalized the first truncated level, which is enough to represent isomorphisms of algebraic structure as equality.
Subject headings
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Keyword
- IDENTITY
- Computer Science
- Theory & Methods
- IDENTITY
Publication and Content Type
- ref (subject category)
- art (subject category)
Find in a library
- Mathematical Structures in Computer Science (Search for host publication in LIBRIS)
To the university's database
- 1 of 1
- Previous record
- Next record
- To hitlist
Find more in SwePub
- By the author/editor
- Barras, B.
- Coquand, Thierry ...
- Huber, Simon, 19 ...
- About the subject
-
- NATURAL SCIENCES
- NATURAL SCIENCES
- and Computer and Inf ...
- Articles in the publication
- Mathematical Str ...
- By the university
- University of Gothenburg
- 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
