Reduction Free Normalisation for a proof irrelevant type of propositions

DOI10.46298/lmcs-19(3:5)2023arXiv2103.04287OpenAlexW3134370287MaRDI QIDQ6135773

Thierry Coquand

Publication date: 26 August 2023

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2103.04287

zbMATH Keywords

normalizationdependent type theorypresheaf models

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Partial Horn logic and Cartesian categories
• Canonicity and normalization for dependent type theory
• A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance
• Pointers in Recursion: Exploring the Tropics
• Types for Proofs and Programs
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Reduction Free Normalisation for a proof irrelevant type of propositions