Session 10A

Chair: Paweł Urzyczyn

• 13:00: Henry DeYoung, Frank Pfenning, Klaas Pruiksma. Semi-Axiomatic Sequent Calculus.     See abstract ...
  ABSTRACT. We present the semi-axiomatic sequent calculus (SAX) that blends features of Gentzen's sequent calculus with an axiomatic formulation of intuitionistic logic. We develop and prove a suitable analogue to cut elimination and then show that a natural computational interpretation of SAX provides a simple form of shared memory concurrency.
• 13:30: Chuangjie Xu. A Gentzen-style monadic translation of Goedel's System T.     See abstract ...
  ABSTRACT. We introduce a syntactic translation of Goedel's System T parametrized by a weak notion of a monad, and prove a corresponding fundamental theorem of logical relation. Our translation structurally corresponds to Gentzen's negative translation of classical logic. By instantiating the monad and the base case of the logical relation, we reveal various properties and structures of T-definable functionals such as majorizability, continuity and bar recursion. Our development has been formalized in the Agda proof assistant.
• 14:00: Mario Alvarez-Picallo, C.-H. Luke Ong. The difference lambda-calculus: a language for difference categories..     See abstract ...
  ABSTRACT. Cartesian difference categories are a recent generalisation of Cartesian differential categories which introduce a notion of infinitesimal arrows satisfying an analogue of the Kock-Lawvere axiom, with the axioms of a Cartesian differential category being satisfied only up to an infinitesimal perturbation. In this work, we construct a simply-typed calculus in the spirit of the differential lambda-calculus equipped with syntactic infinitesimals and show how its models correspond to difference lambda-categories, a family of Cartesian difference categories equipped with suitably well-behaved exponentials.