The stack calculus
Alberto Carraro (PPS, Universit\'e Paris Diderot), Thomas Ehrhard, (PPS, Universit\'e Paris Diderot), Antonino Salibra (DAIS, Universit\`a Ca', Foscari Venezia)
TL;DR
The paper introduces a new functional calculus that faithfully encodes classical logic, ensuring confluence, strong normalization, and soundness, with a straightforward denotational semantics for interpretation.
Contribution
It presents a simple, confluent calculus with a type system guaranteeing strong normalization and full implicational classical logic, along with an accessible denotational semantics.
Findings
Calculus is confluent without restrictions
Type system enforces strong normalization
Complete for full implicational classical logic
Abstract
We introduce a functional calculus with simple syntax and operational semantics in which the calculi introduced so far in the Curry-Howard correspondence for Classical Logic can be faithfully encoded. Our calculus enjoys confluence without any restriction. Its type system enforces strong normalization of expressions and it is a sound and complete system for full implicational Classical Logic. We give a very simple denotational semantics which allows easy calculations of the interpretation of expressions.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.