Deciding equivalence with sums and the empty type

DOI10.1145/3009837.3009901zbMath1387.03014arXiv1610.01213OpenAlexW2529368321MaRDI QIDQ5370875

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

equivalencesaturationfocusingsumscanonicitysimply-typed lambda-calculusempty type

Mathematics Subject Classification ID

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

Related Items (3)

Unnamed Item ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type ⋮ The naturality of natural deduction. II: on atomic polymorphism and generalized propositional connectives

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