Guarded Cubical Type Theory

↓ Direkt till sidans innehåll
↓ Direkt till sidans sekundära innehåll (sidomenyn)

Sökning: onr:"swepub:oai:research.chalmers.se:0754f029-1d52-44c6-8cb1-3d9ad66a5cde" > Guarded Cubical Typ...

1 av 1
Föregående post
Nästa post
Till träfflistan

Birkedal, LarsÅrhus Universitet,Aarhus University (författare)

Guarded Cubical Type Theory

Artikel/kapitelEngelska2019

Förlag, utgivningsår, omfång ...

2018-06-26
Springer Science and Business Media LLC,2019

Nummerbeteckningar

LIBRIS-ID:oai:research.chalmers.se:0754f029-1d52-44c6-8cb1-3d9ad66a5cde
https://research.chalmers.se/publication/510847URI
https://doi.org/10.1007/s10817-018-9471-7DOI

Kompletterande språkuppgifter

Språk:engelska
Sammanfattning på:engelska

Ingår i deldatabas

SwePubSwePub

Klassifikation

Ämneskategori:art swepub-publicationtype
Ämneskategori:ref swepub-contenttype

Anmärkningar

This paper improves the treatment of equality in guarded dependent type theory ((Formula presented.)), by combining it with cubical type theory ((Formula presented.)). (Formula presented.) is an extensional type theory with guarded recursive types, which are useful for building models of program logics, and for programming and reasoning with coinductive types. We wish to implement (Formula presented.) with decidable type checking, while still supporting non-trivial equality proofs that reason about the extensions of guarded recursive constructions. (Formula presented.) is a variation of Martin–Löf type theory in which the identity type is replaced by abstract paths between terms. (Formula presented.) provides a computational interpretation of functional extensionality, enjoys canonicity for the natural numbers type, and is conjectured to support decidable type-checking. Our new type theory, guarded cubical type theory ((Formula presented.)), provides a computational interpretation of extensionality for guarded recursive types. This further expands the foundations of (Formula presented.) as a basis for formalisation in mathematics and computer science. We present examples to demonstrate the expressivity of our type theory, all of which have been checked using a prototype type-checker implementation. We show that (Formula presented.) can be given semantics in presheaves on (Formula presented.), where (Formula presented.) is the cube category, and (Formula presented.) is any small category with an initial object. We then show that the category of presheaves on (Formula presented.) provides semantics for (Formula presented.).

Ämnesord och genrebeteckningar

NATURVETENSKAP Matematik Algebra och logik hsv//swe
NATURAL SCIENCES Mathematics Algebra and Logic hsv//eng
HUMANIORA Filosofi, etik och religion Filosofi hsv//swe
HUMANITIES Philosophy, Ethics and Religion Philosophy hsv//eng
NATURVETENSKAP Matematik Matematisk analys hsv//swe
NATURAL SCIENCES Mathematics Mathematical Analysis hsv//eng
Cubical type theory
Homotopy type theory
Guarded recursion

Biuppslag (personer, institutioner, konferenser, titlar ...)

Bizjak, AlešÅrhus Universitet,Aarhus University (författare)
Clouston, RanaldÅrhus Universitet,Aarhus University (författare)
Grathwohl, Hans BuggeÅrhus Universitet,Aarhus University (författare)
Spitters, BasÅrhus Universitet,Aarhus University (författare)
Vezzosi, Andrea,1986Chalmers tekniska högskola,Chalmers University of Technology(Swepub:cth)vezzosi (författare)
Århus UniversitetChalmers tekniska högskola (creator_code:org_t)

Sammanhörande titlar

Ingår i:Journal of Automated Reasoning: Springer Science and Business Media LLC63:2, s. 211-2530168-74331573-0670

Internetlänk

Hitta via bibliotek

Journal of Automated Reasoning (Sök värdpublikationen i LIBRIS)

Till lärosätets databas

1 av 1
Föregående post
Nästa post
Till träfflistan

Hitta mer i SwePub

Av författaren/redakt...: Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans ...; Spitters, Bas; Vezzosi, Andrea, ...

Om ämnet

NATURVETENSKAP: NATURVETENSKAP; och Matematik; och Algebra och logi ...

HUMANIORA: HUMANIORA; och Filosofi etik oc ...; och Filosofi

NATURVETENSKAP: NATURVETENSKAP; och Matematik; och Matematisk analy ...

Artiklar i publikationen: Journal of Autom ...

Av lärosätet: Chalmers tekniska högskola

Sök utanför SwePub

Sök vidare i:: Google; 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.

LIBRIS.kb.se