2015 Complogic Workshop - July 16th, 2015
McConnell 320, McGill University
10:00am |
Between modal and first-order: hybrid logic 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. |
10:30am |
Contextal Linear LF 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. |
11:00am |
The marriage of effects, monads and Beluga 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? |
11:30am |
Lunch |
1:00pm |
Overview on Krivine's classical realisability 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. |
1:30pm |
A Case Study on Logical Relations using Contextual Types 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. |
2:00pm |
Well-founded Recursion over Contextual Objects 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. |