Deciding equivalence with sums and the empty type

2016/10/04 by Scherer, Gabriel
#03F03 #68N18 #F.3.3 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)

paper · doi:10.48550/arxiv.1610.01213

Abstract

The logical technique of focusing can be applied to the λ-calculus; in a simple type system with atomic types and negative type formers (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 decidability of βη-equivalence in presence of the empty type, the fact that it coincides with contextual equivalence, and a finite model property.

Related

• An extended type system with lambda-typed lambda-expressions (extended version)
• The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010)
• A Reflection Principle for Potential Infinite Models of Type Theory
• Internalization of extensional equality
• Infinitary Intersection Types as Sequences: a New Answer to Klop's Question