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 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 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 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 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 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 |
TBA |
|
November 22nd |
TBA |
|
November 29th |
TBA |
|
December 6th |
TBA |