@inproceedings{91ad0ce0cbf7441ba89b587ecdfb77bc,
title = "Deciding equivalence with sums and the empty type",
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.",
keywords = "Canonicity, Empty type, Equivalence, Focusing, Saturation, Simply-typed lambda-calculus, Sums",
author = "Gabriel Scherer",
note = "Publisher Copyright: {\textcopyright} 2017 ACM.; 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 ; Conference date: 15-01-2017 Through 21-01-2017",
year = "2017",
month = jan,
day = "1",
doi = "10.1145/3009837.3009901",
language = "English",
series = "Conference Record of the Annual ACM Symposium on Principles of Programming Languages",
publisher = "Association for Computing Machinery",
pages = "374--386",
editor = "Gordon, \{Andrew D.\} and Giuseppe Castagna",
booktitle = "POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages",
}