Slides from the talk [pdf]

Joint work with Jeroen Groenendijk, presented at SPE8.

*Abstract:* In this talk I will discuss the interplay between
two important topics in programming language research: dependent types
and computational effects; by defining a small dependently-typed
language, combining the features of Martin-Löf type theory and
computational languages such as Call-By-Push-Value and the Enriched
Effect Calculus. Our language has both value types and terms and
computation types and terms, with the value and computation types only
allowed to depend on values. A novel aspect of our language is the use
of computational sigma-types to account for type-dependency in the
sequential composition of computations.

The design of our language is inspired by a class of categorical models we call fibred adjunction models. These naturally combine i) comprehension categories arising from the semantics of dependent types; and ii) adjunctions arising from the semantics of computational effects. We also discuss a variety of examples, some arising from EM-algebras of monads, some from other decompositions of monads into adjunctions and some from considering general recursion as a computational effect.

Finally, we also comment on some ongoing work on understanding parametrized adjunctions and parametrized computational effects in this fibred setting. In particular, we show how the clear distinction between values and computations sheds new light on how to model parametrized computational effects where the result parameters need to depend on result values, for example, to model the possible failure of opening a file.

This is joint work with Neil Ghani and Gordon Plotkin.

Slides from the talk (shortened version) [pdf]

*Abstract:* We provide a system of polarized proof nets for
the systems FILL- and BILL- (Full Intuitionistic and Bi-Intuitionistic
Linear Logic without units). The sequent calculus formulation of FILL-
and BILL- uses labelled sequents as in (Hyland and De Paiva
1993). Proof nets (Girard 1987) are polarized as in (Bellin and Scott
1994). Polarized directed paths as in Lamarche's essential nets for
intuitionistic linear logic ILL (Lamarche 1994), have been used also
in (Bellin 1997) for FILL- and here for BILL-. The specific
correctness condition for FILL- is called functionality condition on
the representation of linear implication and has a dual constructivity
condition on subtraction for BILL-.

Slides from the talk [pdf]

*Abstract:* Independence-Friendly logic (IF logic) introduced
by Hintikka and Sandu (1989) is an extension of FOL with slashed
quantifiers of the form (∀x/W), (∃x/W), intended to
express the independence of the choice for the existential (universal)
quantifier from the values of the variables in the set W. IF logic
leads to greater expressive power than ordinary FOL and generates such
phenomena as indeterminacy and signaling. We present an overview of
some of the results on expressive power and complexity obtained in the
last years.

Slides from the talk [pdf]

*Abstract:* Relative monads are a naturally arising relaxation
of the monads where the underlying functor need not be an
endofunctor. I will describe relative monads and their surrounding
theory, and give examples of their use in Agda and Haskell.

This is joint work with Thorsten Altenkirch and Tarmo Uustalu, published in a series of papers.

Slides from the talk [pdf]

*Abstract:* This paper tries to remove what seems to be the
remaining stumbling blocks in the way to a full understanding of the
Curry-Howard isomorphism for sequent calculus, namely the questions:
What do variables in proof terms stand for? What is co-control and a
co-continuation? How to define the dual of Parigot's mu-operator so
that it is a co-control operator? Answering these questions leads to
the interpretation that sequent calculus is a formal vector notation
with first-class co-control. But this is just the "internal"
interpretation, which has to be developed simultaneously with, and is
justified by, an equivalent, "external" interpretation, offered by
natural deduction: the sequent calculus corresponds to a
bi-directional, agnostic (wrt. the call strategy), computational
lambda-calculus. Next, the formal duality between control and
co-control is studied, in the context of classical logic. The duality
cannot be observed in the sequent calculus, but rather in a system
unifying sequent calculus and natural deduction.

This work was published in TLCA 2015.

Slides from the talk [pdf]

*Abstract:* Definitions of many mathematical structures used
in computer science are parametrized by finite sets. To work with such
structures in proof assistants, we need to be able to explain what a
finite set is. In constructive mathematics, a widely used definition
is listability: a set is considered to be finite, if its elements can
be listed completely. In this paper, we formalize different variations
of this definition in the Agda programming language. We develop a
toolbox for boilerplate-free programming with finite sets that arise
as subsets of some base set with decidable equality. Among other
things we implement combinators for defining functions from finite
sets and a prover for quantified formulas over decidable properties on
finite sets.

This is joint work with Tarmo Uustalu, it was published in WGP 2015.

Slides from the talk [pdf]

*Abstract:* Functional reactive programming (FRP) is a
programming paradigm that makes it possible to describe the temporal
behavior of a system in a declarative fashion. It has been
independently observed by Alan Jeffrey and myself that FRP types
correspond to temporal logic propositions and FRP expressions
correspond to temporal logic proofs. Subsequent efforts to establish a
precise Curry-Howard isomorphism between FRP and temporal logic have
led to an advanced variant of FRP and a temporal logic that is
intuitionistic. In this talk, I will present this intuitionistic
temporal logic. I will particularly point out how constraints of a
reactive programming setting, such as causality, have motivated design
decisions regarding the logic.

Slides from the talk [pdf]

*Abstract:* We describe work on constructing a complete
implementation of Weispfenning's *virtual term substitution*
method for real closed field formulas of unbounded degree. We build
upon a recent high-performance library for computing over
non-Archimedean real closed fields using Thom's Lemma.

This is joint work with Grant Olney Passmore.

Slides from the talk (shortened version) [pdf]

*Abstract:* In reductive proof search (proof search based on
reduction of conclusions of inference rules to their premises), proofs
are naturally generalised by solutions, comprising all (possibly
infinite) structures generated by locally correct, bottom-up
application of inference rules.

In this talk, we explain the basic ideas of an approach for analysing reductive proof search that builds on the Curry-Howard isomorphism, and rests on the representation not only of individual solutions, but actually of the entire solution space of proof search problems. Two equivalent representations are considered: one through a co-inductive lambda-calculus with sums (where sums capture alternatives in the search process); and the other through a lambda-calculus with sums and fixed points (where fixed points express cycles in the search process). Our case study is intuitionistic implicational logic, and a cut-free sequent calculus proof system (whose proofs are in 1-1- correspondence with simply-typed lambda-terms in eta-long beta-normal form), for which we obtain simple syntax directed recursive procedures to decide existence and (in)finiteness of solutions (avoiding the usual mix of proof search and ad hoc algorithmic control).

This is joint work with José Carlos Espírito Santo and Ralph Matthes, part of it was published in FICS 2013.

Slides from the talk [pdf]

*Abstract:* GF (Grammatical Framework) is a logical framework
based on type theory, with an additional layer of concrete syntax
rules. It was first developed at Xerox Research Centre Europe in 1998
as a tool for domain-specific translation based on semantic
interlinguas defined in type theory. GF has later developed into a
multilingual platform that has grammar libraries for over 30 languages
and supports applications such as mobile speech translators.

The talk will start with a demo of translation and continue with an overview of GF focusing on its origins in logic. It will conclude with a session of live coding in GF's cloud-based grammar editor, in which we will build a small web-based translation system in 20 minutes. The aim of the coding session is to give hands-on understanding of the challenges of grammars and translation.

Slides from the talk [pdf]

*Abstract:* We reformulate the bar recursion and bar induction
principles in terms of recursive and wellfounded coalgebras. Bar
induction was originally proposed by Brouwer as an axiom to recover
certain classically valid theorems in a constructive setting. It
allows us to prove properties of *choice sequences*, that is,
infinite streams of natural numbers, by a form of induction on the
finite paths inside a non-wellfounded tree. Bar recursion, introduced
later by Spector, is the corresponding function definition
principle.

We give a generalization of the principles, by defining the notion of barred coalgebra: a process with a spawning behaviour given by a functor, such that all possible computations terminate.

Bar recursion is the statement that every barred coalgebra is recursive; a recursive coalgebra is one that allows definition of functions by a coalgebra-to-algebra morphism. It is a framework to characterize valid forms of recursion for terminating functional programs.

One application of the principle is the tabulation of continuous functions: Ghani, Hancock and Pattinson defined a type of wellfounded trees that represent continuous functions on streams. Bar recursion allows us to prove that every continuous function can be tabulated to such a tree.

Finally, the principle of coalgebraic bar induction states that every barred coalgebra is wellfounded; a wellfounded coalgebra is one that admits proof by induction.

This is joint work with Venanzio Capretta.

Slides from the talk [pdf]

This is joint work with Tarmo Uustalu and in part with Denis Firsov.

Last update 7 December 2015