Proofs and programs (13 – 17 February)

Talk list

Lectures

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 Martin-Lö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 Martin-Lö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
  • Paul-André 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 type-theoretic 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 so-called "subtoposes" of this topos, and associated notions of realizability. The collection of local operators forms a Heyting algebra into which the upper-semilattice 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 continuation-passing-style (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 lambda-calculus.

    References

    [1] Gilles Barthe, John Hatcliff, 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 Hatcliff, and Morten Heine Sørensen. Cps translations and applications: The cube and beyond. Higher-Order and Symbolic Computation, 12(2):125–170, 1999.

    [3] Thierry Coquand and Hugo Herbelin. A-translation 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 fibred preorders (functors of type Setop → Preord, e.g. triposes or more general hyperdoctrines) to them which abstract their essential features. These fibred 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 fibred preorders is given by those which are represented by ordinary preorders, i.e. are of the form Set(−, D) for a preorder D. The 2-category of representable fibred preorders (being equivalent to the 2-category of preorders and monotone functions) and its relation to categorical logic via presheaf and sheaf constructions is fairly well understood, but the 2-category of general fibred preorders is more difficult to handle. To overcome these difficulties, we introduce basic relational objects (BROs), which are representations of fibred preorders that generalize (and in our opinion simplify) Hofstra’s basic combinatory objects [1]. The 2-category BRO of BROs, which is equivalent to a full sub-2-category of the 2-category of fibred posets, has good closure properties – in particular it has an involution (−)op : BROco → BRO corresponding to fibrewise (−)op on the level of fibred preorders, which allows us to dualize Hofstra’s existential quantification monad D to obtain a monad which classifies universal quantification. Moreover, BRO is sufficiently 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 game-theoretic 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 Montevideo--see [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 “non-constructive” objects.

    • Tuesday 14, 16:15
  • Shin-ya Katsumata (RIMS, Kyoto, Japan), A Generic Soundness Result for Effect Systems.

    Effect system is a type-based approach to statically estimate side effects caused by programs. Such estimation brings various benefits to the analysis and transformation of programs. The purpose of the pioneering work by Lucassen and Gifford [5] was to design the effect system that assists safe scheduling of expressions in parallel computing. Since then, effect system has been widely applied to analysing the behaviour of programs. For instance, control flow analysis can be concisely captured as an effect system [6]. Region-based memory management in functional languages is developed based on the idea of effect 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 effect analysis.

    The variety of effect systems is governed by two factors. The first factor is the side effect implemented in a language, and the second factor is the property about side effects that we estimate by an effect system. Once we choose these factors, we aim to establish the effect soundness, stating that when the effect system asserts that a program P has an effect e, the actual execution of P causes the side effect that satisfies the property described by e.

    This type of argument is common in many works on effect system, but the effect soundness is discussed in individual situations. This naturally leads us to seek for a general effect soundness argument for any kind of side effects. In this work we propose an effect system and discuss the effect soundness without committing into a particular computational effect. The technical contributions are twofold:

    • We design an effect system with effect polymorphism, and give a predicate semantics to it. The basic idea of this semantics is to interpret each type τ as a predicate over the effect-erasure |τ|. To make the effect system rich, we formulate effects (with effect variables) as morphisms in a discrete Lawvere Pos-theory containing the theory of monoid (1, ·). We use this monoid to represent the composition of effects.

    The key concept in the predicate semantics of the effect system is the effect-indexed lifting P of a monad A. It formulates Wadler and Thiemann’s effect-delimited monad [9] in the context of predicate semantics. It maps a pair of an effect 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 effects. 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, effect soundness is discussed under a given description of effects, which is formulated as a mapping from a pair of an effect e and a type τ to a predicate D(e, τ) over the computation of type τ. The effect soundness is then the claim that for any program M of type τ having an effect e, the predicate semantics interprets M as an element in D(e, τ).

    We present a method to construct an effect-indexed lifting from a description of effects. This construction is a variant of ⊤⊤-lifting [4] indexed by effects. We then show that if 1) D(1, τ) contains all pure computations and 2) D is closed under generic effects, then the constructed lifting gives a predicate semantics of the effect system that is sound with respect to D. This result holds for a wide range of strong monads and descriptions of effects.

    References

    [1] N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. Relational semantics for effect- 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 effect- based program transformations: higher-order store. In A. Porto and F. J. L´ pez-Fraguas, 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. Gifford. Polymorphic effect systems. In Proceedings of the 15th ACM SIGPLAN-SIGACT 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 effect-based 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 call-by-value lambda-calculus using a stack of regions. In POPL, pages 188–201, 1994.

    [9] P. Wadler and P. Thiemann. The marriage of effects and monads. ACM Trans. Comput. Log., 4(1):1–32, 2003.

    • Monday 13, 16:30
  • Paul Blain Levy (University of Birmingham), Call-by-push-value: the fine-grained structure of call-by-value and call-by-name .

    Call-by-push-value is a calculus of computational effects that emerges, quite automatically, from an experiment: take simply typed lambda-calculus with either call-by-value (CBV) or call-by-name (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 "fine-grained CBV" calculus with primitives for returning and sequencing. Secondly, CBN and fine-grained CBV each have a decomposition into another calculus, viz. call-by-push-value.

    • Friday 17, 15:00