Sciweavers

ESOP
2016
Springer

Computing with Semirings and Weak Rig Groupoids

7 years 12 months ago
Computing with Semirings and Weak Rig Groupoids
Abstract. The original formulation of the Curry–Howard correspondence relates propositional logic to the simply-typed λ-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-preservi...
Jacques Carette, Amr Sabry
Added 03 Apr 2016
Updated 03 Apr 2016
Type Journal
Year 2016
Where ESOP
Authors Jacques Carette, Amr Sabry
Comments (0)