Martin Aher: Epistemic and deontic questions in the miners' puzzle

Slides from the talk [pdf]

Joint work with Jeroen Groenendijk, presented at SPE8.

Danel Ahman: Fibred computational effects

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.

Gianluigi Bellin: Proof nets / essential nets for FILL- and BILL-

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-.

Fausto Barbero and Gabriel Sandu: Independence-friendly logic: an overview

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.

James Chapman: Relative monads

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.

José Carlos Espírito Santo: Curry-Howard for sequent calculus at last

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.

Denis Firsov: Dependently typed programming with finite sets

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.

Wolfgang Jeltsch: Intuitionistic temporal logic from reactive programming

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.

Kristjan Liiva: Real quantifier elimination by virtual term substitution of unbounded degree

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.

Sara Negri: Glivenko sequent classes in the light of structural proof theory

Sara Negri: Proof theory for Lewis counterfactuals and conditional logic

Luís Pinto: Analysis of proof search through typed lambda-calculi

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.

Aarne Ranta: GF: a logical framework for grammars [tutorial]

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.

Tarmo Uustalu: Coalgebraic bar recursion and bar induction

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.

Niccolò Veltri: Constructive finiteness and rational datatypes

Slides from the talk [pdf]

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

Jan von Plato: How to linearize a tree derivation?

Jan von Plato: In search of the roots of formal computation

Tarmo Uustalu
Last update 7 December 2015