Deciding equivalence with sums and the empty type

Autor: Gabriel Scherer
Přispěvatelé: Northeastern University [Boston], Proof search and reasoning with logic specifications (PARSIFAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France
Jazyk: angličtina
Rok vydání: 2017
Předmět:
FOS: Computer and information sciences
Computer Science - Logic in Computer Science
F.3.3
F.4.1
Pure mathematics
Computer science
0102 computer and information sciences
02 engineering and technology
01 natural sciences
Unit type
Empty sum
03F03
68N18
0202 electrical engineering
electronic engineering
information engineering
0101 mathematics
Equivalence (formal languages)
Equivalence (measure theory)
Computer Science - Programming Languages
Type inhabitation
Simply typed lambda calculus
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
010102 general mathematics
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
16. Peace & justice
Computer Graphics and Computer-Aided Design
Logic in Computer Science (cs.LO)
Decidability
010201 computation theory & mathematics
Algebraic data type
Software
Programming Languages (cs.PL)
Zdroj: POPL 2017
POPL 2017, Jan 2017, Paris, France
POPL
Popis: 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 with set-theoretic equality in all finite models.
Databáze: OpenAIRE
Externí odkaz: