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...

• Type: Journal
• Year: 2016
• Where: ESOP
• Authors: Jacques Carette, Amr Sabry
• Keywords: ESOP 2016, Programming Languages