Skip to main content

Research Repository

Advanced Search

Outputs (3)

Constructing a universe for the setoid model (2021)
Conference Proceeding
Altenkirch, T., Boulier, S., Kaposi, A., Sattler, C., & Sestini, F. (2021). Constructing a universe for the setoid model. In S. Kiefer, & C. Tasson (Eds.), Foundations of Software Science and Computation Structures : 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings (1-21). https://doi.org/10.1007/978-3-030-71995-1_1

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)
Journal Article
Altenkirch, T., & Geniet, C. (2020). Big Step Normalisation for Type Theory. LIPIcs, 2020, Article 4. https://doi.org/10.4230/LIPIcs.TYPES.2019.4

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)
Conference Proceeding
Altenkirch, T., Boulier, S., Kaposi, A., & Tabereau, N. (2019). Setoid Type Theory—A Syntactic Translation. In Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019, Proceedings (155-196). https://doi.org/10.1007/978-3-030-33636-3_7

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.