Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

The Multiverse: Logical Modularity for Proof Assistants

Abstract : Proof assistants play a dual role as programming languages and logical systems. As programming languages, proof assistants offer standard modularity mechanisms such as first-class functions, type polymorphism and modules. As logical systems, however, modularity is lacking, and understandably so: incompatible reasoning principles-such as univalence and uniqueness of identity proofs-can indirectly lead to logical inconsistency when used in a given development, even when they appear to be confined to different modules. The lack of logical modularity in proof assistants also hinders the adoption of richer programming constructs, such as effects. We propose the multiverse, a general type-theoretic approach to endow proof assistants with logical modularity. The multiverse consists of multiple universe hierarchies that statically describe the reasoning principles and effects available to define a term at a given type. We identify sufficient conditions for this structuring to modularly ensure that incompatible principles do not interfere, and to locally restrict the power of dependent elimination when necessary. This extensible approach generalizes the ad-hoc treatment of the sort of propositions in the Coq proof assistant. We illustrate the power of the multiverse by describing the inclusion of Coq-style propositions, the strict propositions of Gilbert et al., the exceptional type theory of Pédrot and Tabareau, and general axiomatic extensions of the logic.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

https://hal.inria.fr/hal-03324596
Contributor : Kenji Maillard Connect in order to contact the contributor
Submitted on : Monday, August 23, 2021 - 5:21:20 PM
Last modification on : Friday, August 5, 2022 - 2:54:52 PM
Long-term archiving on: : Wednesday, November 24, 2021 - 7:04:36 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03324596, version 1

Citation

Kenji Maillard, Nicolas Margulies, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter. The Multiverse: Logical Modularity for Proof Assistants. 2021. ⟨hal-03324596⟩

Share

Metrics

Record views

62

Files downloads

130