Tue 9 Jan 2018 16:00 - 16:30 at Museum A - Formalizing Meta-Theory Chair(s): Brigitte Pientka

We propose a formalization of HO$\pi$ in Coq, a process calculus where messages carry processes. Such a higher-order calculus features two very different kinds of binder: process input, similar to $\lambda$-abstraction, and name restriction, whose scope can be expanded by communication. We formalize strong context bisimilarity and prove it is compatible, i.e., closed under every context, using Howe’s method, based on several proof schemes we developed in a previous paper.

Tue 9 Jan
Times are displayed in time zone: Tijuana, Baja California change

16:00 - 18:00: Formalizing Meta-TheoryCPP at Museum A
Chair(s): Brigitte PientkaMcGill University
16:00 - 16:30
Talk
HOpi in Coq
CPP
Sergueï LengletUniversity of Lorraine, France, Alan SchmittInria
DOI
16:30 - 17:00
Talk
A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
CPP
Paweł WieczorekUniversity of Wrocław, Dariusz BiernackiUniversity of Wrocław
DOI
17:00 - 17:30
Talk
A Two-Level Logic Perspective on (Simultaneous) Substitutions
CPP
Kaustuv ChaudhuriInria, France
DOI
17:30 - 18:00
Talk
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
CPP
Jonas Kaiser, Steven Schäfer, Kathrin StarkSaarland University, Germany
DOI