ProgLog Main
ProgLog Pages
edit SideBar

Programming Logic Seminar
Unless otherwise stated, talks take place at 13:1514:15 in room 8103 (by the lunch room).
(There is a standing booking of room 8103 for Proglog meetings, every Wednesday 13:1514:30, starting 20130724.)
Calendar
UPCOMING TALKS
2015
Jesper Cockx is visiting June 9th to July 18th 2015.
PAST TALKS
2015
 Wednesday April 15, 13:1514:15: Pierre Hyvernat, Continuous functions between streams (et al.) as datatype
Brouwer already knew that continuous functions between streams (equipped with the usual product topology) had a representation in terms of infinite trees. Peter Hancock implemented this idea in dependent type theory and described it figuratively as "eating". He tried generalizing it to more general coinductive types and it is only recently that we succeeded, by using the notion of interaction structure (also called indexed container, or polynomial functor by others).
I will present this work, introducing the necessary concepts on a "by need" basis: coinductive types and continuous functions, polynomial functors, simulations, and inductive/recursive definitions.
This is joint work with Peter Hancock.
 Wednesday March 18, 13:1514:15: JeanPhilippe Bernardy, Focusing by Evaluation
We present an evaluator for Girard's LL, written in Haskell. Based on this evaluator, we construct a focusing algorithm for LL. Remarkably, focusing does not require any modification of the evaluator (one just calls it).
We have used focusing to generate efficient code from LL proofs (resting on the usual proofs as programs interpretation). In fact, focusing and codegeneration proper can be fused to obtain a shorter, and perhaps more clear codegenerator.
Joint work with Victor Lopez Juan.
 Wednesday March 4, 13:1514:15: Peter Dybjer, Undecidability of Equality in the Free Locally Cartesian Closed Category
(joint work with Simon Castellan and Pierre Clairambault)
We show that a version of MartinLöf type theory with extensional identity, a unit type N1, Sigma, Pi, and a base type is a free locally cartesian category on one object in a 2categorical sense. We also show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic.
 Wednesday February 25, 13:1514:15: Magnus Myreen, CakeML: a formally verified compiler for ML
I will present the CakeML project. This project centers around a subset of ML that is carefully chosen to be easy to write programs in and convenient to reason about formally. I will talk about results so far, in particular, our formally verified implementation of CakeML (a compiler and a readevalprint loop) in 64bit x86 machine code. The construction and verification of this implementation required both proofs of highlevel programs (the parser, type inferencer, and compiler) and lowlevel programs (the runtime in x86 machine code, its bignum library, and garbage collector). We used a novel technique to produce much of the verified lowlevel code: we bootstrapped the verified compiler algorithm, within higherorder logic, to produce the verified lowlevel implementation. I will also explain how divergence preservation was proved using simple clocks. This work was carried out using the HOL4 theorem prover.
 Wednesday February 18, 13:1514:15: Víctor López Juan, A classical approach to compositional array programming
Linear logics treat propositions as resources which must be produced or consumed a fixed number of types. This makes them potentially wellsuited for modelling performancesensitive programs.
We use the classical variant of linear logic (CLL, Girard 1987) as the basis for a language in which programs can be composed in a functional style. At the same time, duality and linearity provide a straightforward fusion scheme, and guarantee that its application will not duplicate work. The result is more general than current approaches, which either rely on compiler heuristics or the use of a fixed set of combinators.
In the talk I will briefly describe the logic and our extensions to it. I will then discuss the core ideas behind the compilation strategy. Finally, I will show some examples of array kernels written in the language, and benchmarks thereof.
 Wednesday January 14, 13:1514:15: Andrea Vezzosi, Representation Independent Existential Types in the Presheaf Model of Parametricity
In the "existential" view of parametricity existential types are the tool to define abstract data types, where two different internal representations are still equal if they cannot be told apart with the provided interface. I will present a truncation operation that when applied to Sigma types gives the expected existentials.
In their presheaf model of parametricity Atkey et al. define a universe of discrete reflexive graphs to recover the identity extension lemma. That universe happens to be a reflective subcategory of sheaves and the sheafification functor is the truncation from the general universe of reflexive graphs.
I will then use such existentials to define inductive types a la Guarded Recursive Types.
2014
 Friday December 12: Anders Mörtberg, PhD thesis defense: Formalizing Refinements and Constructive Algebra in Type Theory
 Thursday December 11: Type theory and formalization of mathematics (in kårhuset, Ascom room)
9:30  10:00 Fika 10:00  11:00 MartinLof  Making sense of normalization by evaluation 11:15  12:15 Palmgren  Variants of categories with families and their formalization Abstract: Categories with families (cwfs) is one of the semantical structures for MartinLöf type theory (MLTT) that is closest to the syntax of the theory. Formalizing the notion in type theory it self present some choices, whether to consider cwfs whose equality is interpreted as definitional equality in types and terms, which restricts the number of models, or is interpreted as extensional equality. The latter presents some problems of coherence. We also consider cwfs with named projections and their relation to MartinLöf's Substitution Calculus (1992). This talk presents work in progress. 12:15  13:45 Lunch 13:45  14:45 Gonthier  Constructing Algebraic Numbers While ordinarily algebraic numbers are introduced as a subset of the (classical) complex numbers, it is common folklore that they can also be obtained constructively. However actually constructing algebraics is not so easy, and doing so elegantly and rigorously in a formal proof system is even harder. With R. O'Connor and C. Cohen, we had to revisit constructively several topics in number theory to arrive at a satisfactory resolution. In the process we also got an answer of sorts to another ancient conundrum: isn't the Fundamental Theorem of Algebra really a theorem in Analysis? 15:00  16:00 Lumsdaine  Characterising identity types of inductive types: from 1 ≠ 0 to Blakers–Massey. The “codedecode” method has been one of the most fruitful discoveries in the typetheoretic ("synthetic") development of homotopy theory. It extends traditional typetheoretic characterisations of identity types of inductive types (e.g. decidable equality of booleans and naturals), to similarly characterise or approximate the identity types of higher inductive types, recovering close analogues of various classical homotopytheoretic results. 16:00  16:30 Fika 16:30  17:30 Rasmus Møgelberg  Topos of trees
 Wednesday December 3, 13:1514:15: JeanPhilippe Bernardy, Controlled Array Fusion Using Linear Types
One issue with today's functional languages is that they exhibit unpredictable efficiency: a seemingly harmless refactoring may significantly decrease the efficiency of the compiled code. We attribute this unpredictability to the following tension: on the one hand removal of intermediate data structures (deforestation, or fusion) is critical to the performance of functional programs, but on the other hand fusion is unreliable.
Based on classical linear logic, we present a calculus with reliable fusion, and sufficient to express many arraybased computations. An additional benefit of our design is that parallelism opportunities are made explicit, allowing efficient compilation to parallel architectures.
 Wednesday November 26, 13:1514:15: Simon Huber, Implementing a variation of the cubical set model
I will report on a new implementation of a type checker based on a variation of the cubical set model of type theory. It features function extensionality, the univalence axiom, higher inductive types like the circle or propositional truncation, and the equality for J is definitional.
 Wednesday November 12, 13:1514:15: Andrea Vezzosi, A Formalized Proof of Strong Normalization for Guarded Recursive Types
Nakano's "later" modality allows negative recursive types and guarded general recursion without introducing inconsistencies. The modality has found applications for synthetic stepindexing, enforcing causality in Functional Reactive Programming and ensuring productivity of coinductive definitions. We present a strong normalization proof and its formalization in Agda for a smallstep reduction parametrized by a natural number ``depth'' that expresses under how many guards we may step during evaluation.
 Wednesday November 5, 13:1514:15: Benjamin Pierce, Linguistic Foundations for Bidirectional Transformations
Note: Room changed to EA!
Computing is full of situations where two different structures must be "connected" in such a way that updates to each can be propagated to the other. This is a generalization of the classical view update problem, which has been studied for decades in the database community; more recently, related problems have attracted considerable interest in other areas, including programming languages, software model transformation, user interfaces, and system configuration. Among the fruits of this crosspollination has been the development of a linguistic perspective on the problem. Rather than taking some view definition language as fixed (e.g., choosing some subset of relational algebra) and looking for tractable ways of "inverting" view definitions to propagate updates from view to source, we can directly design new bidirectional programming languages in which every expression denotes a pair of functions mapping updates on one structure to updates on the other. Such structures are often called lenses. The foundational theory of lenses has been studied extensively, and lensbased language designs have been developed in several domains, including strings, trees, relations, graphs, and software models. These languages share some common elements with modern functional languages  in particular, they come with very expressive type systems. In other respects, they are rather novel and surprising. This talk surveys recent developments in the theory of lenses and the practice of bidirectional programming languages.
 Wednesday October 15, 13:1514:15: Francesco Mazzoli, Type checking in the presence of metavariables (reprise)
When treating metavariables in dependently typed languages, the literature usually presents the unification algorithm as a standalone component. However the need to check definitional equality of terms while type checking gives rise to a tight interplay between type checking and unification. We propose an algorithm to express type checking entirely in the form of unification constraints, thus making the whole process significantly more modular and understandable.
 Wednesday October 8, 13:1514:15: Bas Spitters Formalizing Mathematics in the Univalent Foundations
We have been formalizing mathematics in type theory for many years. Although great progress has been made, there were still a number of issues that are hard to tackle, especially when leaving the realm of discrete mathematics. We mention a lack of quotient types and the absence of a clear mathematical semantics for the Coq type theory.
Homotopy type theory promises a solution to these challenges. I will discuss how to develop some mathematics in the univalent foundations and report on the design of our Coq library.
Basic familiarity with type theory and some categorical semantics is assumed.
 Wednesday September 24: Koen Claessen: Automated reasoning for intuitionistic propositional logic using a SATsolver
ABSTRACT: I have built an automated theorem prover for intuitionistic propositional logic, using an existing SATsolver and ~150 lines of Haskell code. The prover is based on applying the idea of Satisfiability Modulo Theories (SMT) *recursively*. SMT is a technique for implementing automated theorem provers that expresses the logic in which we want to prove things as an extension of propositional logic, so that we can use a SATsolver to do the heavy lifting in the propositional part of the logic.
My prover constructs proofs as well as counter models. It beats all existing automated provers on most (existing and new) benchmarks.
The main reasons for giving this presentation are: (1) it is a cool idea that may actually improve your understanding of intuitionistic logic (it certainly improved mine), (2) I want to ask if anyone has any applications of this logic , (3) it may be more useful to extend the ideas to intuitionistic firstorder logic but I don't know how to do this yet and I may need your help.
 Wednesday September 17: Pierry Boutry (University of Strasbourg): On decidability of Tarski's system of geometry
ABSTRACT: In 1948 Alfred Tarski established the decidability of the full first order theory of any instance of real closed field with decidable comparison or any instance of Tarski’s system of geometry with decidable equality. He achieved it by proving the completeness of his quantifier elimination procedure for the first order theory of real closed fields. This procedure was programmed and proved correct and complete in Coq by Cyril Cohen and Assia Mahboubi. Our goal is to prove that this procedure can be applied to Tarski's system of geometry. To do so we first need to prove two statements. First that the first ten axioms of Tarski’s system of geometry are a model of plane over an ordered fields which was recently formalized in Coq by Gabriel Braun. Second that any plane over an ordered field is a model of the first ten axioms of Tarski's system of geometry. We will first recall the axioms of both of these theories. We will then explain the modifications we made to Gabriel Braun's formal proof in order to get a proof which does not rely on the use of the excluded middle. Next we will present our approach for proving the second statement. Finally we will state what will remain to be done to formally prove the completeness of Tarski's system of geometry.
 Wednesday September 10: Florian Rabe (Jacobs University, Bremen): MMT: A FoundationIndependent Approach to Declarative Languages
ABSTRACT: MMT is a framework for representing declarative languages such as logics, type theories, or set theories.
MMT achieves a high level of generality by systematically avoiding a commitment to a particular syntax or semantics.
Instead, individual language features (e.g., lambdaabstraction, conjunction, etc.) are represented as reusable modules, which are composed into concrete languages.
These modules can be declarative by specifying features as MMT theories or programmatic by providing individual rules as plugins.
Despite this high degree of abstraction, it is possible to implement advanced algorithms generically at the MMT level.
These include knowledge management algorithms (e.g, IDE, search, change management) as well as logical algorithms (e.g., parsing, type reconstruction, module system).
Thus, we can use MMT to obtain advanced implementations of declarative languages at extremely low cost.
 Wednesday August 20: Damien Rouhling (ENS Lyon): Universes in dependent type theory: let terms climb the ladder
ABSTRACT: In 2011, Conor McBride wrote a blog post about the possibility of combining cumulativity and universe polymorphism in a dependent type system. He suggested to get cumulativity through a subtyping judgment and to achieve universe polymorphism by using a lifting operator. This operator just increments every universe level in a term and, thus, sends terms of one universe to terms in the next one. One can declare a term of a certain type and then use a lifted version of it when it is needed. I will show a proof of normalization by evaluation for a system in which the lifting operator is a term constructor.
I won't assume any knowledge about normalization by evaluation. Only some familiarity with dependent types will be required from the audience. This will be a 20 minutes talk.
 Wednesday June 25: Damien Rouhling (ENS Lyon): Congruence Closure Modulo a Theory
ABSTRACT: The theory of Equality on Uniterpreted Functions can be combined with another theory. This combination is called the congruence closure of the given theory. In his PhD Stéphane Lescuyer described an algorithm to decide the consistency of a set of equalities and disequalities in such a combination. His approach gets its genericity from the use of a congruence on terms, hence the name congruence closure *modulo*.
I will explain how I have exploited this algorithm to build a decision procedure for an automated prover called PSYCHE.
 Wednesday June 18: Andrea Vezzosi: A Categorical Perspective on Pattern Unification
ABSTRACT: In 1991 Miller described a subset of the higherorder unification problem for the Simply Typed Lambda Calculus which admits most general unifiers, called the pattern fragment. This subset has been extended to more complex type theories and it is still used as the basis of modern unification algorithms in applications like proof search and type inference. I will give a new presentation of the original unification algorithm that focuses on the abstract properties of the operations involved, using category theory as a structuring principle.
 Monday April 7: Rasmus Møgelberg (ITU Copenhagen): Guarded recursion in type theory
ABSTRACT: This talk is about extensions of type theory with guarded recursive types, i.e., recursively defined types in which the recursion variable only appears underneath a modal operator. One motivation for studying these type theories is that the guarded recursive types can be used to construct models of programming languages with advanced notions of state, which can be seen as synthetic variants of models constructed using stepindexing techniques, but unlike these offer a type system for expressing the model constructions. Guarded recursive variants of coinductive types have also been suggested as a way of expressing productivity requirements of coinductive definitions using types.
In the talk I will describe the toposoftrees model of guarded recursion and, if time permits, I’ll discuss intensional models of guarded recursion and relations between guarded recursive types and coinductive types.
 Wednesday April 2: Fabien Renaud (INRIA and Ecole Polytechnique): The ProofCert project
ABSTRACT: In the ProofCert project, we are exploring to what extent we might be able to accommodate a wide range of proof evidence from various provers and then to have independent checkers certify such proof evidence.
In this talk I will present the various aspects of ProofCert as well as the design of the independent checkers, which rely on focused sequent calculi.
 Wednesday March 19: Per MartinLöf (Stockholm University): Dependence and causality
 Wednesday March 12: Thierry Coquand: (Pre)sheaf models of type theory and parametricity
ABSTRACT: We explain what is a presheaf model of type theory and illustrate this with the example of presheaf model over the category of partial bijection. This gives a semantics to the notion of "colors" of JeanPhillipe and Guilhem, and we can also give a semantics to unary parametricity. The model of cubical sets (without the Kan condition) is a variation and gives a semantics to binary parametricity.
 Wednesday February 19: Andrea Vezzosi: Mechanizing Pattern Unification
ABSTRACT: In 1991 Miller described a subset of the higherorder unification problem which admits most general unifiers, called the pattern fragment. This subset is still used as the basis of modern unification algorithms in applications like proof search and type inference. Starting from an intrinsically typed syntax for the Simply Typed Lambda Calculus, I will present a formalization of the original algorithm as an Agda program whose type ensures both soundness and completeness.
In the implementation we'll make use of basic abstractions from category theory to structure our proofs and let the type constraints guide us to find the unifier.
 Wednesday February 12: Fredrik Lindblad: A sequent calculus style of case expressions
ABSTRACT: How to deal with unification combined with iotareduction in agsy was a longlasting issue. A couple of problem examples finally made it clear that the previous hack was not only unappealing but could also lead to performance problems.
I will present an alternative way of representing case expressions and recursive functions, analogous to the way normal application is represented in agsy and agda. With a sequent calculus style of applications (variable head plus list of arguments) syntax prohibits betaredexes. Correspondingly, a sequent calculus style of case expressions prohibits iotaredexes, making unification a cleaner business.
 Wednesday January 29: Thorsten Altenkirch (University of Nottingham): Containers in Homotopy Type Theory
ABSTRACT: Homotopy Type Theory (HoTT) is a new extension of MartinLöf Type Theory which has been proposed as a new foundation of Mathematics. One of its main applications so far has been to use type theory to model constructions in homotopy theory. In this talk I will look at a potential application of HoTT in computer science  more specifically using containers to model datatypes. It turns out that containers give rise to a much richer notion of datatypes in this setting, including multisets and cycles (a list without a beginning). There is an interesting interaction with the notion of a derivative of datatypes in particular the existence of antiderivatives which was investigated by Gylterud.
 Wednesday January 22: Bassel Mannaa: Sheaf model of algebraically closed field extension
ABSTRACT: I’ll briefly present dynamical computation of algebraic numbers. I’ll then present a model of this computation as a sheaf object over the site of finitely presented regular algebras. We also show that the axiom of choice fails for this model.
 Wednesday January 15: JeanPhilippe Bernardy: A sequentcalculus presentation of typetheory
ABSTRACT: We aim to construct a typetheory which can be used as a backend for dependentlytyped languages such as Agda or Coq. Such a language should be  a typetheory: correctness should be expressible via types
 lowlevel: one should be able to translate various highlevel languages into this language while retaining properties such as runtime behaviour, etc.
 minimal: the typechecking program should be amenable to verification.
Functional programming (FP) languages have long used sequentcalculus based presentations for their lowlevel representations (or the closely related CPS), as they are close to hardware, while retaining the essential properties of FP.
I will outline our prototype implementation of a sequentcalculus presentation of typetheory:
 syntax
 translation from a 'natural syntax'
 evaluation
 'definitional' equality
 typechecking
 examples
2013
 Wednesday December 18: Thierry Coquand: An implementation of univalence
ABSTRACT: Together with Anders, Cyril and Simon, we have implemented computations for type theory with univalence (and propositional truncation). This implementation takes a closed term of this extension of type theory and computes its value in the cubical set model. If this term is of type Nat we get a numeral as a result (but the computation may use higher dimensional object during the computation). In particular we can transport structures along isomorphisms. I will do a demo of the system.
 Wednesday December 4: Fabien Renaud: Some Insights into focusing
ABSTRACT: Focusing was originally presented as an efficient search procedure for linear logic. I will first introduce focusing as a way to constrain the shape of the proofs in different logics and discuss the different presentations found in the literature. Then I will show how focusing can be useful in logic programming (to specify the chaining method used); in functional programming (to specify evaluation orders); and if I have time, some other recent applications.
 Wednesday November 27: Cyril Cohen: Refinements for free! (j.w.w. Maxime Dénès and Anders Mörtberg)
ABSTRACT: Formal verification of algorithms often requires a choice between definitions that are easy to reason about and definitions that are computationally efficient. One way to reconcile both consists in adopting a highlevel view when proving correctness and then refining stepwise down to an efficient lowlevel implementation. Some refinement steps are interesting, in the sense that they improve the algorithms involved, while others only express a switch from data representations geared towards proofs to more efficient ones geared towards computations. We relieve the user of these tedious refinements by introducing a framework where correctness is established in a prooforiented context and automatically transported to computationoriented data structures. Our design is general enough to encompass a variety of mathematical objects, such as rational numbers, polynomials and matrices over refinable structures. Moreover, the rich formalism of the Coq proof assistant enables us to develop this within Coq, without having to maintain an external tool.
 Wednesday November 20: Anders Mörtberg: A Coq formalization of finitely presented modules (j.w.w. Cyril Cohen)
ABSTRACT: The use of vector spaces in homology theory does not give the same information as with Rmodules. A generalization to finitely presented modules covers computable Zhomology, which gives more finegrained topological invariants. We formalize a construction of finitely presented modules over coherent and strongly discrete rings and discuss its properties. This formalization gives basic building blocks that lead to a clean definition of homology groups.
 Wednesday November 13: Andreas Abel: Pattern inductive families need not store their indices, ever  Or: On polymorphic type theory, with an application to proof term compression
ABSTRACT: We review monomorphic type theory with unidirectional type inference and contrast it to bidirectional type checking, a technique somewhat related to polymorphic type theory.
We present a few ideas for term compression stemming from bidirectional type checking, in particular ideas from Edwin Brady's "Inductive families need not store their indices" (TYPES 2003) and Jason Reed's "Redundancy Elimination for LF" (LFMTP 2004), the latter a clarification of George Necula and Peter Lee's "Efficient Representation and Validation of Proofs" (LICS 1998). We review the current partial implementation of these ideas in Agda's internal syntax and outline opportunities to put them to their full use (with potential to reduce the term size by the square root). We give a demonstration of their implementation in MiniAgda (under construction).
This is an informal talk with halfbaked results.
 Wednesday November 6: Dan Rosén: Write and type check Agda code in your browser
ABSTRACT: I will show my prototype implementation of a web browser editor for Agda. It supports some of the most important features from the emacs interface: syntax highlighting, type checking, refining, case split and auto. This is a shorter talk, open for discussions about future directions.
 Wednesday October 30: Åse Fahlander: The correspondence between the universe à la Russell and the universe à la Tarski in MartinLöf type theory
ABSTRACT: It is generally assumed that type theory with universe(s) formulated a´ la Russell and type theory with universe(s) formulated a´ la Tarski are closely connected  rather two different ways of writing things than two different theories. I will present a proof that there is indeed a onetoone correspondence between the derivable judgements in a version of type theory with one universe formulated a´ la Russell, and those derivable judgements in a corresponding version formulated a´ la Tarski that are irreducible with respect to a weak form of reduction. It also follows that there is a onetoone correspondence between those derivable judgements in each theory that are irreducible with respect to ordinary reduction. The theories concerned are intensional and polymorphic, with untyped conversion in place of equality. The proof could probably be extended to cover other versions of type theory with one universe, but does not readily extend to multiple universes.
 Wednesday October 16: Iliano Cervesato: Towards MetaReasoning in the Concurrent Logical Framework CLF
ABSTRACT: The concurrent logical framework CLF is an extension of the logical framework LF designed to specify concurrent and distributed languages. While it can be used to define a variety of formalisms, reasoning about such languages within CLF has proved elusive. In this talk, we describe ongoing work towards defining an extension of LF that allows us to express properties of CLF specifications. We illustrate the approach with a proof of safety for a small language with a parallel semantics.
 Wednesday September 11: Roy Crole: Nominal Lambda Calculus
ABSTRACT: Reasoning about atoms (names) is difficult. The last decade has seen the development of numerous novel foundations, theories and techniques. Our work is founded on nominal sets and the slightly more general notion of FMSets.
In the first part of the talk we shall give a brief introduction to FMsets, expressing our ideas in the language of category theory. We shall try to give a range of concrete examples and to motivate the main part of the talk, which concerns what we term the Nominal Lambda Calculus.
Theories in equational logic (also known as (simple) algebraic theories, or theories for equational reasoning) have been studied for many years. Clouston and Pitts introduced Nominal Equational Logic, which provides judgements both of expression equality, and of freshness of atoms. Just as Equational Logic can be enriched with function types to yield the lambdacalculus, we have developed Nominal Lambda Calculus (NLC) by enriching NEL with (atomdependent) function types and abstraction types.
In the second part of the talk we introduce pure NLC and look in detail at some the the rules of the NLC formal system. We show that NLC is sound by giving a categorical semantics, explaining some of the complexities that arise from a dependent type system. We then consider completeness and illustrate that we cannot define a complete categorical semantics for pure NLC. However, by adding in a novel form of dependently typed atom abstraction, we get a system that is complete. We demonstrate some of the rules for such atom abstraction, and outline how the problem with completeness can be solved in a neat manner.
 Wednesday September 4: Simon Huber: A Model of Type Theory in Cubical Sets
ABSTRACT: I will present a model of type theory in a constructive metatheory. The model is based on cubical sets and can be seen as a constructive version of the Kan simplicial set model of type theory; the main difference to the simplicial set model is a strengthening of the Kan filling conditions.
 Thursday June 20 at 14:15 in 6128: Koen Claessen will talk about SMT solvers
Koen will say something about "the implementation of SMT solvers, how they are used, what their relationship is with full firstorder logic provers, and so on".
 Wednesday June 12: Cyril Cohen: A theory of contractible contexts
 Wednesday May 7: Cyril Cohen: Formalization of algebraic numbers in Coq
ABSTRACT: In this talk I show a formalization in Coq of real and complex algebraic numbers together with their structure of real closed field and algebraically closed field. These numbers are useful in the recently achieved formalization of the proof of the odd order theorem (aka FeitThompson theorem), where they substitute for real and complex numbers. In this proof, it is mandatory to know the partial order structure on complex numbers. This leads to build complex algebraics on top of real algebraic numbers.
The construction of real algebraic numbers is based on a construction of Cauchy reals, in particular to define arithmetic operations. I will show the methodology we used to do epsilondela proof in a comfortable way. The final step of this construction involves a quotient, which we show how to perform. Finally, the construction of complex algebraic numbers and their order structure is done by extending real algebraic numbers with the imaginary element i and the proof of algebraic closure is the fundamental theorem of algebra.
 Wednesday April 22 at 15:15 in 6128: Nicolas Pouillard: Constructive Probabilistic Reasoning
Joint work with Daniel Gustafsson.
ABSTRACT: We present how to constructively reason about probabilistic functions in the Type Theory of Agda. We aim at being able to reason about security in for example evoting protocols. Here, a lightweight model is constructed where probabilistic functions are presented as deterministic functions with an extra argument for the randomness. We build a generalised form of summation functions for a large collection of finite types. These summation functions exhibit a large quantity of derived properties, arising from two fundamental properties that these functions should have.
 Wednesday March 27: Peter Ljunglöf: Typebased HumanComputer Interaction
ABSTRACT: (This is an idea that I will present on the TYPES meeting in April. Since I've never been there before, I hope that you can give me lots of tips on how I can improve my presentation.)
A dialogue system is a computer system that can engage in dialogue with a human in order to complete tasks such as answering questions or performing actions.
Aarne Ranta and Robin Cooper described how a dialogue system can be implemented in a typetheoretic proof assistant. Metavariables in the proof tree represent questions that needs to be answered by the user. However, their theory is rather simple and yields a formbased dialogue system that cannot handle underspecified answers, anaphoric expressions, or ambiguous utterances.
We extend their theory with ideas from linguistic theories of dialogue and syntax, to make the system handle more flexible dialogues. Ranta and Cooper use focus nodes to know which of the nodes in the tree that is the current question under discussion. To this we add the idea of unfixed nodes from Dynamic Syntax. An unfixed node is a subtree which we know should be attached somewhere below a given node, but we do not yet know exactly where. We use unfixed nodes for representing underspecified answers, which is a very common phenomenon occuring in everyday dialogue between human participants.
The general idea of the dialogue manager is to ask the user to refine the current focus node. User utterances are then translated to (possibly incomplete) subtrees, which the system tries to incorporate into the dialogue tree. If the user utterance is of the same type as the focused metavariable, the tree can be extended directly. Otherwise the system will try to add the utterance as an unfixed node below the focus, or it will try to change focus to another metavariable that has a compatible type. There are (at least) three possible refinement strategies for deciding which node to select as the next focus, corresponding to different dialogue behaviour: I call them topdown, bottomup and bottomdown refinement.
The ideas of metavariables and focus nodes is borrowed from the Agda proof assistant. Hopefully the new additions of unfixed nodes and refinement strategies can be borrowed back, and be used for making proof assistants more intuitive to use.
 Wednesday Feb 20 in 8103: Johan Glimming: EU Project Proposal on Constructive Programming, http://www.functor.se/research/seminarfeb2013/
 Wednesday Jan 30 in 5128: Cyril Cohen and Peter Dybjer: What's going on in Princeton?
 Friday Jan 18: 1300  1400 Stevan Andjelkovic, Strathclyde University, will give a talk in 5128 about his PhD work.
 Friday Jan 11: Henrik Nilsson, University of Nottingham, UK: Functional Programming Gets Physical
ABSTRACT: Equational models of physical phenomena and systems is essentially noncausal in the sense that the equations state the relation among the involved entities: there are no a priori assumptions about which entities are "known" and which are "unknown", needing to be computed from the known ones. However, making use of such models, for example, predicting the behaviour of a system through simulation, has traditionally required a manual reformulation into causal form to make the computation of unknowns from knowns explicit. This causal reformulation can be very cumbersome, especially for large models. This has led to the development of modelling and simulation languages that directly support a noncausal formulation, obviating the need for manual causalisation. This also turns out to give additional important methodological and modularity benefits.
However, the current industrialstrength noncausal modelling and simulation languages have a number of limitations, notably when it comes to describing hybrid systems: systems that exhibit both continuoustime and discretetime characteristics. In this talk, I'll outline a novel approach to noncausal modelling and simulation of hybrid systems, called Functional Hybrid Modelling (FHM), aimed at mitigating some of these limitations. As the name suggests, it draws from functional programming; in particular, it can be seen as a generalisation of Functional Reactive Programming (FRP), which allows very general hybrid systems to be described, except only causally. I will also briefly discuss our ongoing work on formalising parts of the static and dynamic semantics of FHMtype languages using Agda as a metalanguage.
2012
 Wednesday Nov 7: Cyril Cohen: Metaprogramming in Coq using Canonical Structures and Type Classes
ABSTRACT: In Coq there are two different mechanisms for inferring more than standard type inference could do, through hints given by the user: Canonical Structure and Type Classes. Their implementation differ a lot, and the way to use them is also quite different. I will try to give some insight on how the mathematical component team [1] instrumented canonical structures to build a hierarchy of algebraic structures [2,3] and compare their approach to the math classes [4,5] approach.
 http://www.msrinria.inria.fr/Projects/mathcomponents/
 Packaging Mathematical Structures, François Garillot, Georges Gonthier, Assia Mahboubi and Laurence Rideau
 Generic Proof Tools And Finite Group Theory, François Garillot
 http://mathclasses.org/
 Type classes for mathematics in type theory, Bas Spitters and Eelis van der Weegen
 Wednesday Oct 31: JeanPhilippe Bernardy: Typetheory in color
ABSTRACT: For a long time, there has been support for erasure in the Coq proof assistant: erasing proofs/propositions yield mere programs/types. So far, programs obtained like this have remained completely separated from the world of proofs: one cannot reason about erased programs within Coq. I propose a design to remedy this issue. An immediate consequence is improved potential for reuse in dependentlytyped programs and libraries.
Depending on interest/time I will move on to advanced applications:
 Increased logical power (parametricity)
 higherdimensional aspects
 connections with equality and isomorphism
 noncomputational function space (and equality variant based on it)
 other aspects that might arise in the discussion
 Wednesday Oct 24: Nils Anders Danielsson: Isomorphism implies equality
ABSTRACT: I will talk about an application of the univalence axiom. Take two monoids whose underlying types are "sets" (which means, roughly, that the corresponding identity types are proofirrelevant). If these monoids are isomorphic—meaning that there is a bijective homomorphism from one to the other—then the univalence axiom implies that the monoids are equal. Note that the situation is different in set theory, in which isomorphic monoids are not (in general) equal.
The result can be generalised to a large class of algebraic structures. For details, see http://homotopytypetheory.org/2012/09/23/isomorphismimpliesequality/.
This is joint work with Thierry Coquand.
 Wednesday Oct 17: ChienChung Huang, Max Planck Institute for Computer Science, Saarbrücken: NearPopular Matchings in the Roommates Problem
ABSTRACT: Our input is a graph G = (V, E) where each vertex ranks its neighbors in a strict order of preference. The problem is to compute a matching in G that captures the preferences of the vertices in a popular way. Matching M is more popular than matching M' if the number of vertices that prefer M to M' is more than those that prefer M' to M. The unpopularity factor of M measures by what factor any matching can be more popular than M. We show that G always admits a matching whose unpopularity factor is O(log V), and such a matching can be computed in linear time. In our problem the optimal matching would be a least unpopularity factor matching. We will show that computing such a matching is NPhard. In fact, for any ε, it is NPhard to compute a matching whose unpopularity factor is at most 4/3  ε of the optimal.
 Wednesday Sep 19: Nils Anders Danielsson: Halfbaked talk: Correctbyconstruction prettyprinting
ABSTRACT: I'll describe a correctbyconstruction framework for prettyprinting. The idea is to start with a grammar, and to see prettyprinter "documents" as annotated parse trees.
 Wednesday Sep 5: Laurent Théry: Geometric Algebras: a formalisation
ABSTRACT: We present a formalisation of geometric algebras that has been done in the Coq proof assistant.
For this, we have built a computational model of geometric algebras and show that it has all the required properties. From this model, we have derived an automatic procedure to prove problems in plane projective geometry.
 Wednesday May 30: Fredrik Lindblad: A Deductive System Designed for Proof Search in HOL
ABSTRACT: We have developed a variant of Agsy aimed for higherorder logic, called AgsyHOL. I will present the deductive system which the theorem prover is based on. The system is mainly characterized by a sequent calculus style of elimination and an equality judgment which alternates between normalization and reasoning by equality chains. The soundness of the system, with respect to Church's simple type theory, has been formalized in Agda. I will also mention some implementation details and the empirical result on the TPTP higherorder problems, although not so much has changed since my last presentation.
 Wednesday April 4: Krasimir Angelov: Types in Grammatical Framework
ABSTRACT: In this talk I will outline the current status of the support for dependent types in GF and I will point out the differences and the similarities between GF and Agda. After that I will show why type checking and proof search in type theory are important for natural language applications. The presentation will mostly cover features that are already available but I will also mention the new challenges that we encounter when we try to combine the logic based approach of type theory with statistical language processing.
 Wednesday March 28 at 15:00, probably in 6128: Thierry Coquand: models of type theory with extensional equality
ABSTRACT: I will present work in progress with Simon giving a constructive version of Voevodsky's Kan simplicial set model of type theory. This provides a way to implement a typechecker for type theory with an identity type which satisfies the axiom of extensionality (with the required canonicity property). Some extensions (axiom of univalence, propositional reflection) seem possible.
 Wednesday March 21: Discussion about universes and universe polymorphism
 Wednesday March 7: Peter Dybjer: Tests, games, and MartinLöf's meaning explanations for intuitionistic type theory..
ABSTRACT: 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.
 Wednesday February 15: Dimitrios Vytiniotis: Stop when you are AlmostFull: adventures in constructive termination
(Joint work with Thierry Coquand and David Wahlstedt.)
 Wednesday January 25 in 6128: Guilhem Moulin: A computational interpretation of parametricity, Cont.
 Wednesday January 18: Guilhem Moulin: A computational interpretation of parametricity
(Joint work with JeanPhilippe Bernardy)
ABSTRACT: Reynolds' abstraction theorem has recently been extended to lambdacalculi with dependent types. In this paper, we show how this theorem can be internalized. More precisely, we describe an extension of Pure Type Systems with a special parametricity rule (with computational content), and prove fundamental properties such as ChurchRosser's and strong normalization. All instances of the abstraction theorem can be both expressed and proved in the calculus itself. Moreover, one can apply parametricity to the parametricity rule: parametricity is itself parametric.
 Tuesday January 10 at 11:15 in 6128: Marc Bezem: A set that is streamless but not provably noetherian
ABSTRACT: Coquand and Spiwack recently coined the concepts streamless and noetherian as constructive notions, classically equivalent to finiteness. Noetherian implies streamless, and Coquand and Spiwack conjectured the existence of a set that is streamless but not provably noetherian (all in the constructive sense).
In this talk we present an example of such a set, which is highly undecidable. This result leads to a more difficult question: the existence (or not) of an arithmetical or even decidable set with such properties.
2011
2010
 Wednesday 24th of November, Fredrik Lindblad: Auto in Agda.
ABSTRACT: The Auto command has been around in Agda for about a year. In the latest release it was formally announced. In this talk I'll summarize the technology behind the proof search. Then I'll show how to use the command. Different ways of using it are accompanied by examples. Finally, I'll report on an experiment we did on the higherorder subset of the TPTP problems. The results show that the performance of our approach in comparable to other systems solving HOL problems.
 Wednesday 17th of November, Ana Bove: 10 Years of Partiality and General Recursion.
ABSTRACT: In this talk I will present the invited talk I gave at DTP2010 in Edinburgh during FLoC.
Constructive type theory (CTT), even if originally developed for formalising mathematics, has been seen as a programming language with dependent types for the past 30 years.
CTT is a theory of total functions. This clearly rules out genuine partial function. Most systems based on CTT only allow structurally recursive functions as a way to guarantee totality. These limitations are really a problem when we are faced with the task of formalising and proving correct a function that do not satisfy the requirements.
The search for methodologies to simplify the formalisation of general recursive and partial function in CTT has been a hot topic during the last decade. Many ideas of different nature have been developed in order to facilitate the definition of this class of functions and their subsequent proof of correctness. However, the issue of how to best formalise recursive and partial functions is far from being resolved.
In this talk we will have a look at some of the methodologies that have been popularised in the last few years. We will mainly concentrate on methodologies available for systems like Coq and Agda, but we will also discuss some of the methodologies available for Isabelle/HOL. Though Isabelle/HOL is not based on CTT but on classical highorder logic, functions should be total in Isabelle/HOL if one is to use to system as a theorem prover.
 Wednesday 3rd of November, JP Bernardy: Realizability and Parametricity in PTSs.
ABSTRACT: We describe a systematic method to build a logic from any programming language described as a Pure Type System (PTS). The formulas of this logic express properties about programs. We define a parametricity theory about programs and a realizability theory for the logic. The logic is expressive enough to internalize both theories. Thanks to the PTS setting, we abstract most idiosyncrasies specific to particular type theories. This confers generality to the results, and reveals parallels between parametricity and realizability. If time allows, I will also discuss the implications of the construction on the design of dependently typed languages and proof assistants.
 Wednesday 27th of October, Andrew Pitts: Nominal sets, part II.
ABSTRACT: This is the second of two talks about the category of nominal sets as a place for modelling computation on structures involving names and namebinding operations. A copy of the slides for this seminar are available at <http://www.cl.cam.ac.uk/users/amp12/talks/nominalsets2.pdf>. Recommended reading: "Structural Recursion with Locally Scoped Names", which is available at <http://www.cl.cam.ac.uk/~amp12/papers/strrls/strrls.pdf>.
 Wednesday 20th of October at 11.00, Discussion about important research problems in type theory.
 Wednesday 20th of October, Andrew Pitts: Nominal sets, part I.
 Tuesday 5th of October in the EDIT room, Andrew Pitts: Semantics of Scope.
ABSTRACT: This talk concerns the operational semantics of programming constructs involving locally scoped names. Typically such semantics involves stateful \emph{dynamic allocation}: a set of currentlyused names forms part of the state and upon entering a scope the set is augmented by a new name bound to the the scoped identifier. (Deallocation of names upon leaving a scope is sometimes appropriate too.) More abstractly, one can see this as a transformation of local scopes by expanding them outward to a(n implicit) toplevel.
By contrast, in a neglected paper from POPL 1994, Martin Odersky gave a stateless lambda calculus with locally scoped names whose dynamics contracts scopes inward. The properties of "Oderskystyle" local names are quite different from dynamically allocated ones. The former enjoy much nicer equational properties up to contextual equivalence than the latter. However, it is not so clear, until now, what is the expressive power of Odersky's system.
Here we show that Oderskystyle local names provide a direct semantics of scope from which the dynamicallocation semantics of scope can be obtained by continuationpassing translation. More precisely, we show that there is a cps translation of typed lambda calculus with dynamically allocated names (the PittsStark nucalculus) into Odersky's $\lambda\nu$calculus that is computationally adequate with respect to contextual equivalence in the two calculi.
This is joint work with Steffen Loesch.
 Wednesday 16th of June, Marc Lasson: Internalized realizability in pure type systems.
ABSTRACT: Let P be any pure type system, we are going to show how we can extend P into a PTS P' which will be used as a proof system whose formulas express properties about sets of terms of P. We will show that P' is (strongly) normalizable if and only if P is. Given a term t in P and a formula F in P', P' is expressive enough to construct a formula "t ⊩ F" that is interpreted as "t is a realizer of F". We then prove the following adequation lemma: if F is provable then by projecting its proof back to a term t in P we obtain a proof that "t ⊩ F". Finally, we will present the relation between this realizability construction and JeanPhilippe's work on Reynold's parametricity in PTS.
 Wednesday 9th of June, Koen Claessen: Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models.
ABSTRACT: Induction proofs often fail because the stated theorem is noninductive, in which case the user must strengthen the theorem or prove auxiliary properties before performing the induction step. (Counter)model finders are useful for detecting nontheorems, but they will not find any counterexamples for noninductive theorems. We explain how to apply a wellknown concept from firstorder logic, nonstandard models, to the detection of noninductive invariants. Our work was done in the context of the proof assistant Isabelle/HOL and the counterexample generator Nitpick. This is joint work with Jasmin Blanchette.
 Wednesday 14th of April in the EDIT room, Bob Constable: Recent Advances in Computational Type Theory.
ABSTRACT: Computational Type Theory (CTT) is a theory of computation that has been implemented in the Nuprl and MetaPRL theorem provers. It is in the same family as MartinLof's Intuitionistic Type Theory (ITT) implemented in Agda and the Calculus of Induction Constructions (CIC) implemented in Coq.
The Nuprl system has been used to specify, develop, and verify software systems, to prove theorems in constructive mathematics, and to solve open problems in mathematics. The type system of CTT is explicitly designed to capture concepts used in modern software systems including distributed systems.
This lecture will examine some of the new type constructors and computational primitives added to CTT over the past seven years including dependent intersection types, subtyping, unguessable atoms, and processes. I will discuss how the process type allows us to implement the notion of constructive proofs as processes.
 Wednesday 28th of April in 5128, Pierre Clairambault: Game semantics.
 Thursday 29th of April at 13.15 in the Philosophy Department, Olof Wijksgatan 6 (Gamla Hovrätten), room T340, David Wahlstedt (discussion leader): Truth and Provability.
 Wednesday 5th of May, JeanPhilippe Bernardy: Parametricity in Agda, Inductive definitions and Extensional equality.
ABSTRACT: We extend Reynolds' abstraction theorem to an Agdalike type system. Issues related to inductive definitions and extensionality will be discussed.
 Wednesday 26th of May, Miroslav Dobsicek: On analogies between physics, topology, logic and computation.
ABSTRACT: I will present a recent paper by John C. Baez and M. Stay: Physics, Topology, Logic and Computation: A Rosetta Stone. http://arxiv.org/abs/0903.0340/
PREVIOUS YEAR'S TALKS
Other past talks can be found at the old pages
