Previous seminar schedules are archived here.

Fall 2017 - Complogic Weekly Meetings

Every Wednesday from 3:00pm to 4:30pm

McConnell 103, McGill University

This semester, we will meet up weekly. During those meetings, members of the labs will each speak for around 10 minutes to discuss their current project and on going progress. Then, on select weeks, one person will give a 25 minutes talk to discuss their work more in depth. The schedule for the talks, together with title and abstract will appear here.

September 20th

POPLMark Reloaded
Brigitte Pientka (joint work with Andreas Abel and Alberto Momigliano)

As a follow-up to the POPLMark Challenge, we propose a new benchmark for machine-checked metatheory of programming languages: establishing strong normalization of a simply-typed lambda-calculus with a proof by Kripke-style logical relations. We believe that this case-study overcomes some of the limitations of the original challenge and highlights, among others, the need of native support for context reasoning and simultaneous substitutions.

September 27th

Programming and Reasoning about Infinite Structures
David Thibodeau (joint work with Andreas Abel, Brigitte Pientka, Anton Setzer, and Andrew Cave)

We discuss the representation of infinite data via coinduction, the dual of induction, and introduce copatterns as a syntactic representation for it. We show an extension of copatterns allowing coinductive reasoning about finite data and how proofs are realized in this setting. We conclude by a discussion about the challenges of reasoning coinductively about infinite data in the proposed setting.

October 4th

Indexed Reactive Programming
Stefan Knudsen

Linear temporal logic (LTL) is a logic for reasoning about time. In addition to expressing that some property P holds at some point in time, LTL can specify that P always hold, that it will eventually hold, or that it will hold until some other property Q holds. Under the Curry-Howard correspondance, LTL corresponds to functional reactive programming, a paradigm for stream processing, which has a first-class treatment of both functions and time. First order logic corresponds to indexed types under this correspondance, which allows types to depend on terms from some index language. We introduce "Jackrabbit", a functional reactive programming language with indexed types and present a few programs motivating its use.

October 18th

Weakening in Simple Type Theory
Masahiko Sato

We formulate the Curry-style simple type theory using the map/skeleton representation of untyped lambda terms introduced in [Sato et al. 2013]. The map/skeleton representation enables us to respresent lambda abstraction without using variables.

We illustrate the usefulness of our approach by showing the admissiblity of the weakening rule of the simple type theory.

We will also compare the notions of categorical judgment and hypothetical judgment using the map/skeleton representation.

[Sato et al. 2013] Sato, M., Pollack, R., Schwichtenberg, H. and Sakurai, T., Viewing lambda-terms through maps, Indagationes Mathematicae 24, 1073 - 1104, 2013.

November 1st

From CIC with universes to HOL through Dedukti
François Thiré

Today, we observe a large diversity of proof systems. This diversity has the negative consequence that a lot of theorems are proved many times. Unlike programming languages, it is difficult for these systems to co-operate because they do not implement the same logic. Logical frameworks are a class of theorems provers that overcome this issue by their capacity of implementing various logics. In this work, we use the logical framework Dedukti to transform arithmetic proofs encoded in CIC with universes to HOL.

This transformation is cut in several smaller transformations such as removing universes, dependent products... But for the moment, some transformations are automatic, other has been done manually. The purpose of this talk is to explain how it would be possible to make the whole process fully automatic.

November 15th

Shawn Otis

November 22nd

Vincent Archambault-Bouffard

November 29th

Aliya Hameer

December 6th

Jacob Errington