Classical Notions of Computation and the Hasegawa-Thielecke Theorem
In the spirit of the Curry-Howard correspondence between proofs and programs, we define and study a syntax and semantics for classical logic equipped with a computationally involutive negation, using a polarised effect calculus, the linear classical L-calculus. A main challenge in designing a denotational semantics for the calculus is to accommodate both call-by-value and call-by-name evaluation strategies, which leads to a failure of associativity of composition. In order to tackle this issue, we define a notion of adjunction between graph morphisms on non-associative categories, which we use to formulate polarized and non-associative notions of symmetric monoidal closed duploid and of dialogue duploid. We show that they provide a direct style counterpart to adjunction models: linear effect adjunctions for the (linear) call-by-push-value calculus and dialogue chiralities for linear continuations, respectively. In particular, we show that the syntax of the linear classical L-calculus can be interpreted in any dialogue duploid, and that it defines in fact a syntactic dialogue duploid. As an application, we establish, by semantic as well as syntactic means, the Hasegawa-Thielecke theorem, which states that the notions of central map and of thunkable map coincide in any dialogue duploid (in particular, for any double negation monad on a symmetric monoidal category).
Thu 15 JanDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 15:40 | |||
14:00 25mTalk | Classical Notions of Computation and the Hasegawa-Thielecke Theorem POPL Éléonore Mangel Univ. Paris Cité - CNRS - Inria, Paul-André Melliès Univ. Paris Cité - CNRS - Inria, Guillaume Munch-Maccagnoni INRIA DOI | ||
14:25 25mTalk | From Semantics to Syntax: A Type Theory for Comprehension Categories POPL Niyousha Najmaei École Polytechnique, Niels van der Weide Radboud University, Benedikt Ahrens Delft University of Technology, Paige Randall North Utrecht University DOI | ||
14:50 25mTalk | Higher-Order Behavioural Conformances via Fibrations POPL Henning Urbat Friedrich-Alexander-University Erlangen-Nürnberg DOI | ||
15:15 25mTalk | What Is a Monoid? POPL DOI | ||