A TERM ASSIGNMENT FOR DUAL INTUITIONISTIC LOGIC. (2009)
Gianluigi Bellin, Nicola Gambino, Maria Emilia Maietti, Kurt Ranalter, Edmund Robinson
Abstract. We study the proof-theory of co-Heyting algebras and present a calculus of continuations typed in the disjunctive–subtractive fragment of dual intuitionistic logic. We give a...
Categorical proof theory of classical propositional calculus (2008)
Gianluigi Bellin, Martin Hyland, Edmund Robinson, Christian Urban C
We investigate semantics for classical proof based on the sequent calculus. We show that the propositional connectives are not quite well-behaved from a traditional categorical perspective, and give...
King's Buildings, Edinburgh EH9 3JZ Scotland (2007)
We develop a notion of equivalence between interpretations of the simply typed -calculus together with an equationally de ned abstract data-type, and we show that two interpretations are equivalent...
Categorical Proof Theory of Classical Propositional Calculus (2005)
Gianluigi Bellin, Martin Hyland, Edmund Robinson, Christian Urban C
We investigate semantics for classical proof based on the sequent calculus. We show that the propositional connectives are not quite well-behaved from a traditional categorical perspective, and give...
Proof Nets for Classical Logic (2003)
This paper introduces a notion of proof net for classical logic, provides a static correctness condition for these nets, and analyses theconnection between nets and conventional sequent calculus. The...
Logical relations and data abstraction (1996)
Abstract. We prove, in the context of simple type theory, that logical relations are sound and complete for data abstraction as given by equational speci cations. Specically, we show that two...
Variations on algebra: monadicity and generalisations of equational theories (1994)
Rod Burstall gave me my rst academic job. This was, he explained, to help his group learn about some of the more advanced aspects of category theory. In fact I spent much of my time learning from...
Parametricity as Isomorphism (1993)
Edmund Robinson, Edmund Robinson
. We investigate a simple form of parametricity, based on adding "abstract" copies of pre-existing types. Connections are made with the Reynolds-Ma theory of parametricity by logical...