The stack calculus
Logic in Computer Science
2013-04-01 v1
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.
Keywords
Cite
@article{arxiv.1303.7331,
title = {The stack calculus},
author = {Alberto Carraro and Thomas Ehrhard and Antonino Salibra},
journal= {arXiv preprint arXiv:1303.7331},
year = {2013}
}
Comments
In Proceedings LSFA 2012, arXiv:1303.7136