Proofs and programs (13 – 17 February)
Talk list
Lectures

Hugo Herbelin (INRIA, Paris, France).
 Monday 13, 11:00 — Classical logic and control operators
 Thursday 16, 11:00 — Proving with delimited control
 Friday 17, 11:00 — On the use of side effects in logic

Guy McCusker (Bath, UK),
Strategies and programs.
 Tuesday 14, 9:00
 Wednesday 15, 9:00

Alexandre Miquel (ENS Lyon, France),
Classical realizability.
 Tuesday 14, 11:00 — Introduction to classical realizability
 Wednesday 15, 11:00 — Models induced by classical realizability

Gordon Plotkin (Edinburgh, UK),
Introduction to the algebraic theory of effects.
 Thursday 16, 9:00
 Friday 17, 9:00
Invited talks

Ulrich Berger (Swansea, UK),
Extracting concrete programs from abstract mathematics.
In this talk I will argue that in order to extract correct and useful programs from mathematical proofs it is often not necessary to completely formalize the objects considered, but only certain carefully chosen aspects of them. This makes the formalization of mathematical objects and proofs for the purpose of program extraction a much less daunting enterprise than one might expect, and brings this method of certified program development closer to practical applications. I will illustrate this by means of examples in constructive analysis.
 Monday 13, 15:00

Peter Dybjer (Chalmers University),
Tests, games, and MartinLöf's meaning explanations for intuitionistic type theory..
In this talk I shall argue that program testing provides the basis for constructive mathematical truth. This point of view leads to a modification of MartinLöf's meaning explanations for intuitionistic type theory, where the judgements of type theory are viewed as conjectures which can be tested in order to be corroborated or refuted. In particular we get a new interpretation of hypothetical judgments, since tests for such judgments need methods for generating inputs. We sketch a "test manual" for intuitionistic type theory which employs concepts from game semantics, for example, input generation corresponds to opponent's moves in a game. In order to test a typing judgement we simultaneously play a strategy generated by a type and a strategy generated by a term, where the correct moves for the strategy of the term are determined dynamically by playing the strategy of the type.
The talk is on joint work in progress with Pierre Clairambault, Cambridge.
 Monday 13, 14:00

PaulAndré Melliès (CNRS, Paris, France),
Tensorial logic with algebraic effects.
Tensorial logic is a primitive logic of tensor and negation which refines linear logic by relaxing the hypothesis that negation is involutive. I will explain how the logic provides a typetheoretic foundation to game semantics, and how it may be extended with algebraic effects in order to recover specific categories of games and strategies.
 Friday 17, 14:00

Thomas Streicher (Darmdstadt, Germany),
The Classical Realizability Tripos and Topos.
After recalling basic notions from tripos theory and classical realizability we show how classical realizability gives rise to a tripos and ensuing topos. Finally we pose some questions about assemblies which facilitate the study of realizability models over pca's but seem to be much more difficult in case of classical realizability.
 Tuesday 14, 14:00

Jaap van Oosten (Utrecht, Netherlands),
Local Operators in the Effective Topos.
Local operators in the effective topos correspond to socalled "subtoposes" of this topos, and associated notions of realizability. The collection of local operators forms a Heyting algebra into which the uppersemilattice of Turing degrees embeds; in that respect it is similar to (the dual of) the Medvedev lattice. The talk aims to introduce the audience to this structure and to some techniques for doing calculations in it.
It is based on joint work by Sori Lee and the speaker.
 Thursday 16, 14:00
Contributed talks

Pierre Boutillier,
Delimited Control and Continuation Passing Style in Pure Type Systems.
Pure Type Systems provide with a generic framework at the intersection of proof theory and programming languages for studying arbitrary type systems over the dependent product type. The power of expressivity is made by an appropriate choice of sorts, of axioms for typing sorts and of rules for governing the formation of dependent products.
The syntax of Pure Type Systems mixes terms and types in the same syntactical category. This forbids continuationpassingstyle (cps) transformations in their full generality. Therefore, control operators do not behave correctly with dependent types in general. Logically sound restrictions of dependently typed frameworks with control operators have been successfully exhibited by Coquand and Herbelin [3] and by Barthe, Hatcliff and Sørensen [1, 2] by restricting the sorts where control can occur. (It allows the cps transformation only on objects living in types whose sort does not type another sort.)
We propose a new kind of restriction thanks to delimited control. Delimiters provide a way to go out of the cps monad under certain circumstances. We use them each time we need to staunch the calculus. To ensure that the correct circumstances hold, product types are annotated with return types and we use a annotated typing system that comes forward from the cps transformation and follows what Danvy and Filinski[4] made in the simply type lambdacalculus.
References
[1] Gilles Barthe, John Hatcliﬀ, and Morten Heine Sørensen. A notion of classical pure type system. Electr. Notes Theor. Comput. Sci., 6:4–59, 1997.
[2] Gilles Barthe, John Hatcliﬀ, and Morten Heine Sørensen. Cps translations and applications: The cube and beyond. HigherOrder and Symbolic Computation, 12(2):125–170, 1999.
[3] Thierry Coquand and Hugo Herbelin. Atranslation and looping combinators in pure type systems. Journal of Functional Programming, 4(1):77–88, 1994.
[4] Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. Technical Report 89/12, DIKU, University of Copenhagen, Copenhagen, Denmark, August 1989.
 Thursday 16, 15:30

Jonas Frey,
Basic relational objects and partial combinatory algebras.
Categorical logic attempts to understand realizability constructions by asso ciating ﬁbred preorders (functors of type Setop → Preord, e.g. triposes or more general hyperdoctrines) to them which abstract their essential features. These ﬁbred preorders can then be analyzed using various tools and constructions such as categories of partial equivalence relations, assemblies and exact completions. A special class of of ﬁbred preorders is given by those which are represented by ordinary preorders, i.e. are of the form Set(−, D) for a preorder D. The 2category of representable ﬁbred preorders (being equivalent to the 2category of preorders and monotone functions) and its relation to categorical logic via presheaf and sheaf constructions is fairly well understood, but the 2category of general ﬁbred preorders is more diﬃcult to handle. To overcome these diﬃculties, we introduce basic relational objects (BROs), which are representations of ﬁbred preorders that generalize (and in our opinion simplify) Hofstra’s basic combinatory objects [1]. The 2category BRO of BROs, which is equivalent to a full sub2category of the 2category of ﬁbred posets, has good closure properties – in particular it has an involution (−)op : BROco → BRO corresponding to ﬁbrewise (−)op on the level of ﬁbred preorders, which allows us to dualize Hofstra’s existential quantiﬁcation monad D to obtain a monad which classiﬁes universal quantiﬁcation. Moreover, BRO is suﬃciently large to contain all triposes. We argue that BROs provide a good conceptual framework to understand and relate the constructions of exact completion, assemblies and partial equiv alence relations, and to understand the relation to the (pre)sheaf theoretic con structions in the representable case. Furthermore, the framework of basic relational objects permits to give an extensional characterization of realizability over partial combinatory algebras.
References
[1] P.J.W. Hofstra. All realizability is relative. In Mathematical Proceedings of the Cambridge Philosophical Society, volume 141, pages 239–264. Cambridge Univ Press, 2006.
 Thursday 16, 16:15

Mauricio Guillermo,
Specifying arithmetical formulae in classical realizability.
We present the specification problem, which consists in the characterization of the universal realizers of a given formula in terms of its computational behaviour this work is strongly related to the results appearing in [1].
After recalling the theoretical framework of Classical Realizability and giving some simple examples on specification, we present two gametheoretic characterizations of universal realizers of arithmetical formulae.
First, we deal with the case where the language of realizers does not contain instructions incompatible with substitutive constants (in the sense of [1]). For this particular case, we generalize the result proven in [2] for an arbitrary number of alternations of quantifiers. This generalization is part of the work of E. Miquey during his internship at Montevideosee [3].
Second, we present the general case, whitout any assumptions about the instructions allowed in the language of classical realizers. This case, as in [1], must be trated with a more sophisticated game and the proof of the specification leans strongly on the Threads Method introduced in [2] and improved in [1].
References
[1]"Specifying Peirce's Law in Classical Realizability". M. Guillermo & A. Miquel. To appear in MSCS.
[2]"Realizability games in arithmetical formulae". M Guillermo. PhD Thesis 2008.
[3] "Realizing Arithmetical Formulae". E. Miquey. Internship 2011.
 Tuesday 14, 15:30

Guilhem Jaber,
Forcing the Calculus of Construction to get Generalized Inductive Types.
(Joint work with N. Tabareau)
In this talk, I will present an extension of the Calculus of Construction (the theory behind Coq) which allows to extend modularly the type system with new constructors and new inference rules. The idea is to define a translation between the new system and the original one, following the idea of Krivine and Miquel to study the translation of proofs induced by forcing. Here, our translation of forcing will in fact be an internalization in the type theory of the topos of presheaves of Birkedal et al.
I will then show how we can use this technique to allow negative occurence in the inductive types of Coq. Finally, if time permits, I will talk about how to use the forcing method to extend the type system with “nonconstructive” objects.
 Tuesday 14, 16:15

Shinya Katsumata (RIMS, Kyoto, Japan),
A Generic Soundness Result for Effect Systems.
Eﬀect system is a typebased approach to statically estimate side eﬀects caused by programs. Such estimation brings various beneﬁts to the analysis and transformation of programs. The purpose of the pioneering work by Lucassen and Giﬀord [5] was to design the eﬀect system that assists safe scheduling of expressions in parallel computing. Since then, eﬀect system has been widely applied to analysing the behaviour of programs. For instance, control ﬂow analysis can be concisely captured as an eﬀect system [6]. Regionbased memory management in functional languages is developed based on the idea of eﬀect system [8]. A series of papers [3, 1, 2, 7] study a semantic foundation of some aggressive program transformations that depends on the results of eﬀect analysis.
The variety of eﬀect systems is governed by two factors. The ﬁrst factor is the side eﬀect implemented in a language, and the second factor is the property about side eﬀects that we estimate by an eﬀect system. Once we choose these factors, we aim to establish the eﬀect soundness, stating that when the eﬀect system asserts that a program P has an eﬀect e, the actual execution of P causes the side eﬀect that satisﬁes the property described by e.
This type of argument is common in many works on eﬀect system, but the eﬀect soundness is discussed in individual situations. This naturally leads us to seek for a general eﬀect soundness argument for any kind of side eﬀects. In this work we propose an eﬀect system and discuss the eﬀect soundness without committing into a particular computational eﬀect. The technical contributions are twofold:
 We design an eﬀect system with eﬀect polymorphism, and give a predicate semantics to it. The basic idea of this semantics is to interpret each type τ as a predicate over the eﬀecterasure τ. To make the eﬀect system rich, we formulate eﬀects (with eﬀect variables) as morphisms in a discrete Lawvere Postheory containing the theory of monoid (1, ·). We use this monoid to represent the composition of eﬀects.
The key concept in the predicate semantics of the eﬀect system is the eﬀectindexed lifting P of a monad A. It formulates Wadler and Thiemann’s eﬀectdelimited monad [9] in the context of predicate semantics. It maps a pair of an eﬀect e and a predicate X over I to a predicate P(e, X) over AI. Although P(e, −) is not a monad at each e, it collectively behaves as a monad when we move e inside the poset of eﬀects. The main axiom that guarantees this behaviour is that the multiplication µ of A maps the elements satisfying P(e, P(e′ , X)) into P(e · e′ , X).
 Typically, eﬀect soundness is discussed under a given description of eﬀects, which is formulated as a mapping from a pair of an eﬀect e and a type τ to a predicate D(e, τ) over the computation of type τ. The eﬀect soundness is then the claim that for any program M of type τ having an eﬀect e, the predicate semantics interprets M as an element in D(e, τ).
We present a method to construct an eﬀectindexed lifting from a description of eﬀects. This construction is a variant of ⊤⊤lifting [4] indexed by eﬀects. We then show that if 1) D(1, τ) contains all pure computations and 2) D is closed under generic eﬀects, then the constructed lifting gives a predicate semantics of the eﬀect system that is sound with respect to D. This result holds for a wide range of strong monads and descriptions of eﬀects.
References
[1] N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. Relational semantics for eﬀect based program transformations with dynamic allocation. In M. Leuschel and A. Podelski, editors, PPDP, pages 87–96. ACM, 2007.
[2] N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. Relational semantics for eﬀect based program transformations: higherorder store. In A. Porto and F. J. L´ pezFraguas, o editors, PPDP, pages 301–312. ACM, 2009.
[3] N. Benton, A. Kennedy, M. Hofmann, and L. Beringer. Reading, writing and relations. In N. Kobayashi, editor, APLAS, volume 4279 of Lecture Notes in Computer Science, pages 114–130. Springer, 2006.
[4] S. Katsumata. A semantic formulation of ⊤⊤lifting and logical predicates for computa tional metalanguage. In Proc. CSL ’05, volume 3634 of LNCS, pages 87–102. Springer, 2005.
[5] J. M. Lucassen and D. K. Giﬀord. Polymorphic eﬀect systems. In Proceedings of the 15th ACM SIGPLANSIGACT symposium on Principles of programming languages, POPL ’88, pages 47–57, New York, NY, USA, 1988. ACM.
[6] F. Nielson, H. R. Nielson, and C. Hankin. Principles of program analysis (2. corr. print). Springer, 2005.
[7] J. Thamsborg and L. Birkedal. A kripke logical relation for eﬀectbased program transfor mations. In M. M. T. Chakravarty, Z. Hu, and O. Danvy, editors, ICFP, pages 445–456. ACM, 2011.
[8] M. Tofte and J.P. Talpin. Implementation of the typed callbyvalue lambdacalculus using a stack of regions. In POPL, pages 188–201, 1994.
[9] P. Wadler and P. Thiemann. The marriage of eﬀects and monads. ACM Trans. Comput. Log., 4(1):1–32, 2003.
 Monday 13, 16:30

Paul Blain Levy (University of Birmingham),
Callbypushvalue: the finegrained structure of callbyvalue and callbyname .
Callbypushvalue is a calculus of computational effects that emerges, quite automatically, from an experiment: take simply typed lambdacalculus with either callbyvalue (CBV) or callbyname (CBN) operational semantics, and add a variety of effects. Construct denotational semantics for each of the resulting languages, and see what correspondences exist between the various models. Then make the corresponding pieces into the primitives of a new language.
By this method, we firstly see that CBV has a decomposition into a "finegrained CBV" calculus with primitives for returning and sequencing. Secondly, CBN and finegrained CBV each have a decomposition into another calculus, viz. callbypushvalue.
 Friday 17, 15:00