Outputs (3)

Constructing a universe for the setoid model (2021)
Presentation / Conference Contribution
Altenkirch, T., Boulier, S., Kaposi, A., Sattler, C., & Sestini, F. (2021, March). Constructing a universe for the setoid model. Presented at 24th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2021), Online

The setoid model is a model of intensional type theory that validates certain extensionality principles, like function extensionality and propositional extensionality, the latter being a limited form of univalence that equates logically equivalent pr... Read More about Constructing a universe for the setoid model.

Big Step Normalisation for Type Theory (2020)
Presentation / Conference Contribution
Altenkirch, T., & Geniet, C. Big Step Normalisation for Type Theory. Presented at 25th International Conference on Types for Proofs and Programs (TYPES 2019), Oslo, Norway

Big step normalisation is a normalisation method for typed lambda-calculi which relies on a purely syntactic recursive evaluator. Termination of that evaluator is proven using a predicate called strong computability, similar to the techniques used to... Read More about Big Step Normalisation for Type Theory.

Setoid Type Theory—A Syntactic Translation (2019)
Presentation / Conference Contribution
Altenkirch, T., Boulier, S., Kaposi, A., & Tabereau, N. (2019, October). Setoid Type Theory—A Syntactic Translation. Presented at 13th International Conference on Mathematics of Program Construction (MPC 2019), Porto, Portugal

We introduce setoid type theory, an intensional type theory with a proof-irrelevant universe of propositions and an equality type satisfying functional extensionality and propositional extensionality. We justify the rules of setoid type theory by a s... Read More about Setoid Type Theory—A Syntactic Translation.