Skip to Main content Skip to Navigation
Conference papers

Deciding equivalence with sums and the empty type

Gabriel Scherer 1, 2
2 PARSIFAL - Proof search and reasoning with logic specifications
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
Abstract : The logical technique of focusing can be applied to the λ-calculus; in a simple type system with atomic types and negative type form-ers (functions, products, the unit type), its normal forms coincide with βη-normal forms. Introducing a saturation phase gives a notion of quasi-normal forms in presence of positive types (sum types and the empty type). This rich structure let us prove the decidabil-ity of βη-equivalence in presence of the empty type, the fact that it coincides with contextual equivalence, and a finite model property.
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download

https://hal.inria.fr/hal-01646064
Contributor : Scherer Gabriel <>
Submitted on : Thursday, November 23, 2017 - 3:33:25 PM
Last modification on : Thursday, March 5, 2020 - 6:35:45 PM

File

finite-sums.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01646064, version 1
  • ARXIV : 1610.01213

Collections

Citation

Gabriel Scherer. Deciding equivalence with sums and the empty type. POPL 2017, Jan 2017, Paris, France. ⟨hal-01646064⟩

Share

Metrics

Record views

188

Files downloads

209