Accepted Contributions

Contributions

Icon

Native Type Theory 250.49 KB 15 downloads

Christian Williams and Michael Stay ...
Icon

Normalization for multimodal type theory 231.94 KB 7 downloads

Daniel Gratzer ...
Icon

Novel rules of β-conversion in partial type theory 350.09 KB 10 downloads

Jiřı́ Raclavský and Petr Kuchyňka ...
Icon

On the logical structure of choice and bar induction principles 295.47 KB 6 downloads

Nuria Brede and Hugo Herbelin ...
Icon

Proof terms for generalized classical natural deduction 242.05 KB 11 downloads

Herman Geuvers and Tonny Hurkens ...
Icon

Quantitative polynomial functors 253.57 KB 6 downloads

Georgi Nakov and Fredrik Nordvall Forsberg ...
Icon

Quotient inductive-inductive types in the setoid model 277.93 KB 10 downloads

Ambrus Kaposi and Zongpu Xie ...
Icon

Semantic Analysis of Normalization by Evaluation for Fitch-Style Modal Lambda Calculi 288.74 KB 10 downloads

Nachiappan Valliappan, Fabian Ruch, and Carlos Tomé Cortiñas ...
Icon

Semisimplicial Types in Internal Categories with Families 293.22 KB 7 downloads

Joshua Chen and Nicolai Kraus ...
Icon

Simulating large eliminations in Cedille 208.17 KB 12 downloads

Christopher Jenkins, Andrew Marmaduke, and Aaron Stump ...
Icon

Size-Based Termination for Non-Positive Types 331.78 KB 11 downloads

Yuta Takahashi ...
Icon

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq 156.58 KB 9 downloads

Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo...
Icon

Syntax for two-level type theory 209.02 KB 17 downloads

Roberta Bonacina and Benedikt Ahrens ...
Icon

The syntactic tale of the oracle and the trees A model of continuity in a dependent setting 334.49 KB 10 downloads

Martin Baillon and Pierre-Marie Pédrot ...
Icon

Towards Automation for Iris 227.53 KB 9 downloads

Ike Mulder and Robbert Krebbers ...
Icon

Type theories without contexts 189.72 KB 24 downloads

Andrej Bauer and Philipp G. Haselwarter ...