Thierry Coquand - Reduction Free Normalisation for a proof irrelevant type of propositions

lmcs:8818 - Logical Methods in Computer Science, July 13, 2023, Volume 19, Issue 3 - https://doi.org/10.46298/lmcs-19(3:5)2023
Reduction Free Normalisation for a proof irrelevant type of propositionsArticle

Authors: Thierry Coquand

    We show normalisation and decidability of convertibility for a type theory with a hierarchy of universes and a proof irrelevant type of propositions, close to the type system used in the proof assistant Lean. Contrary to previous arguments, the proof does not require explicitly to introduce a notion of neutral and normal forms.

    https://doi.org/10.46298/lmcs-19(3:5)2023
    Source: arXiv.org:2103.04287
    Volume: Volume 19, Issue 3
    Published on: July 13, 2023
    Accepted on: May 1, 2023
    Submitted on: December 9, 2021
    Keywords: Computer Science - Logic in Computer Science
    Licence: Attribution 4.0 International (CC BY 4.0)

    Classifications

    Mathematics Subject Classification 20201
    Sources:
    • [1] zbMATH Open.

    Share and export

    Consultation statistics

    This page has been seen 1721 times.
    This article's PDF has been downloaded 425 times.