definitional inversion 1dependent type theory 1domain theory 1injectivity 1non-normalising systems 1
From the 1 of 2 linked papers with an AI index.
2 papers
cs.LO2026
Definitional Inversion, Without Normalisation
Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu +3
The paper presents a domain‑theoretic proof technique that establishes definitional inversion properties (injectivity and no‑confusion) of type constructors in dependent type syste…
cs.PL2024
Reimplementing Mizar in Rust
Mario Carneiro
This paper describes a new open-source proof processing tool, mizar-rs, a wholesale reimplementation of core parts of the Mizar proof system, written in Rust. In particular, the "c…