Name
Abstract | ||
|---|---|---|
The original formulation of the Curry---Howard correspondence relates propositional logic to the simply-typed $$\\lambda $$λ-calculus at three levels: the syntax of propositions corresponds to the syntax of types; the proofs of propositions correspond to programs of the corresponding types; and the normalization of proofs corresponds to the evaluation of programs. This rich correspondence has inspired our community for half a century and has been generalized to deal with more advanced logics and programming models. We propose a variant of this correspondence which is inspired by conservation of information and recent homotopy theoretic approaches to type theory. Our proposed correspondence naturally relates semirings to reversible programming languages: the syntax of semiring elements corresponds to the syntax of types; the proofs of semiring identities correspond to reversible programs of the corresponding types; and equivalences between algebraic proofs correspond to meaning-preserving program transformations and optimizations. These latter equivalences are not ad hoc: the same way semirings arise naturally out of the structure of types, a categorical look at the structure of proof terms gives rise to at least a weak rig groupoid structure, and the coherence laws are exactly the program transformations we seek. Thus it is algebra, rather than logic, which finally leads us to our correspondence. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-662-49498-1_6 | ESOP |
Field | DocType | Volume |
Program transformation,Monoidal category,Algebra,Computer science,Type theory,Propositional calculus,Algorithm,Theoretical computer science,Mathematical proof,Homotopy,Syntax,Semiring | Conference | 9632 |
ISSN | Citations | PageRank |
0302-9743 | 3 | 0.42 |
References | Authors | |
12 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jacques Carette | 1 | 358 | 38.45 |
| Amr Sabry | 2 | 520 | 35.46 |