Deciding equivalence with sums and the empty type

DOI10.1145/3009837.3009901MaRDI QIDQ5370875zbMATH OpenOpenAlexFDO

Authors Gabriel Scherer

Publication date 20 October 2017

Published in Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1610.01213

zbMATH Keywords

canonicityempty typeequivalencefocusingsaturationsimply-typed lambda-calculussums

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: The logical technique of focusing can be applied to the $lambda$-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.

Recommendations

• scientific article; zbMATH DE number 2185660
• scientific article; zbMATH DE number 814613
• Extensional Rewriting with Sums
• The exp-log normal form of types: decomposing extensional equality and representing terms compactly
• Polarised intermediate representation of lambda calculus with sums

Cited in

(13)

• The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives
• Which simple types have a unique inhabitant?
• Polarised intermediate representation of lambda calculus with sums
• The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type
• Dual-context calculi for modal logic
• Multi-focusing on extensional rewriting with sums
• The exp-log normal form of types: decomposing extensional equality and representing terms compactly
• Checking Emptiness of Non-Deterministic Regular Types with Set Operators
• Intensional harmony as isomorphism
• Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms
• Positive focusing is directly useful
• The Yoneda reduction of polymorphic types
• A new conjecture about identity of proofs

This page was built for publication: Deciding equivalence with sums and the empty type

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5370875)