On Irrelevance and Algorithmic Equality in Predicative Type Theory (Q2881097)

From MaRDI portal
Revision as of 09:28, 19 April 2024 by Importer (talk | contribs) (‎Changed an Item)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
scientific article
Language Label Description Also known as
English
On Irrelevance and Algorithmic Equality in Predicative Type Theory
scientific article

    Statements

    title
    On Irrelevance and Algorithmic Equality in Predicative Type Theory (English)
    0 references
    author
    Andreas Abel
    0 references
    Gabriel Scherer
    0 references
    publication date
    3 April 2012
    0 references
    zbMATH Keywords
    dependent types
    0 references
    proof irrelevance
    0 references
    typed algorithm equality
    0 references
    logical relation
    0 references
    universal Kripke model
    0 references
    describes a project that uses
    Cayenne
    0 references
    Agda
    0 references
    Coq
    0 references

    Identifiers

    zbMATH DE Number
    6021346
    0 references
    arXiv ID
    1203.4716
    0 references
     
    Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Item:Q2881097&oldid=33565087"
    Powered by MediaWiki