Previous seminar schedules are archived here.

2015 Complogic Workshop - July 16th, 2015

McConnell 320, McGill University


Between modal and first-order: hybrid logic
Agata Murawska

The basic concepts of hybrid logic were introduced by Arthur N. Prior in his work on tense logics. The novel idea was to treat time instants as propositions. Hybrid logic has since been adapted for numerous variants of modal, temporal and description systems. Not only can it increase the expressive power of the underlying logic, it may also make the resulting system better behaved in terms of proof theoretic properties. In principle, any kind of logic can be "hybridised" by adding a new kind of propositions: nominals, which are true at exactly one point of a model.

In this talk I'm going to give an overview of hybrid logic, the new operators it introduces as well as its applications. In particular, I will present Hybrid Logical Framework, a framework for linear logic developed by Jason Reed. HLF, as the name suggests, uses a variant of hybrid logic as its foundation. Finally, I will also discuss a generalisation of HLF that we are currently working on at ITU.


Contextal Linear LF
Shawn Otis

While the logical framework LF is well understood and has been implemented in many programming and reasoning frameworks, there are systems for which it is not well suited. Examples of this come in the form of Resources, Session Types and Stateful systems, which are growing in popularity. In order to model these systems, one solution is to consider a linear logical framework, which allows us to limit the usage of assumptions, an intrinsic property of these systems.

We are interested in the meta-theoretic properties of such systems. However, a framework for this does not, to our knowledge, exist. We would thus like to incorporate this linear framework as an extension to Beluga, taking advantage of its two-level approach. Although this contains some additional constructs, such as context variables, which result in design challenges due to their properties in a linear setting, they also allow us to prove theorems involving contexts, which are an important aspect of a linear system.


The marriage of effects, monads and Beluga
Francisco Ferreira

In this talk, I will discuss the Philip Wadler's paper "The marriage of effects and monads" from the point of view of a Beluga user. The talk will mostly discuss how one goes trying to understand a paper using Beluga. It will be a talk with Category Theory, programming languages and friendly cetacea, what's not to like?




Overview on Krivine's classical realisability
Nicolas Jeannerod

Before 1990, there's a strong limitation to the Curry-Howard correspondance: it is restricted to constructive logic, where proof explicitly build the objects that they introduce.

In 1990, Timothy Griffin removes this restriction and extends the correspondance to classical logic by adding the **callcc** operator. Even if some control operators had been introduced earlier, Thimothy Griffin is the first to type a control operator, showing a deep connection between **callcc** and the Pierce's law.

Following this result, various techniques have been introduced to encompass classical logic into computation. Jean Louis Krivine's classical realizability stands among them, and will be the topic of this talk.


A Case Study on Logical Relations using Contextual Types
Andrew Cave

Proofs by logical relations play a key role in establishing rich properties such as normalization or contextual equivalence. They are also challenging to mechanize. In this paper, we describe the completeness proof of algorithmic equality for simply typed lambda-terms by Crary where we reason about logically equivalent terms in the proof environment Beluga. There are three key aspects we rely upon: 1) we encode lambda-terms together with their operational semantics and algorithmic equality using higher-order abstract syntax 2) we directly encode the corresponding logical equivalence of well-typed lambda-terms using recursive types and higher-order functions 3) we exploit Beluga’s support for contexts and the equational theory of simultanous substitutions. This leads to a direct and compact mechanization, demonstrating Beluga’s strength at formalizing logical relations proofs.


Well-founded Recursion over Contextual Objects
Brigitte Pientka

We present a core programming language that supports writing well-founded structurally recursive functions using simultaneous pattern matching on contextual LF objects and contexts. The main technical tool is a coverage checking algorithm that also generates valid recursive calls. To establish consistency, we define a call-by-value small-step semantics and prove that every well-typed program terminates using a reducibility semantics. Based on the presented methodology we have implemented a totality checker as part of the programming and proof environment Beluga where it can be used to establish that a total Beluga program corresponds to a proof.