FSCD 2020: INTERNATIONAL CONFERENCE ON FORMAL STRUCTURES FOR COMPUTATION AND DEDUCTION
PROGRAM FOR FRIDAY, JULY 3RD
Days:
previous day
next day
all days

View: session overviewtalk overview

13:00-14:00 Session 7: Invited speaker: A. Pitts (all times are in CEST timezone - UTC+2)
13:00
Quotients in Dependent Type Theory

ABSTRACT. Constructs that involve taking a quotient are commonplace in mathematics.  Here I will consider how they are treated within dependent type theory.  The notion of quotient type has its origins in the Nuprl theorem-proving system for extensional type theory. Later Hofmann formulated a version for intensional type theory in his thesis. This depends on having a pre-existing notion of intensional identity type. Hofmann used Martin-L\"of's notion, the indexed family inductively generated from proofs of reflexivity.  The recent homotopical view of identity in terms of path types gives a more liberal perspective and has brought with it the notion of higher inductive type (HIT), subsuming both inductive and quotient types.  Inductively defined indexed families of types (in all their various forms) are perhaps the most useful concept that dependent type theory has contributed to the practice of computer assistance for formalizing mathematical proofs. However, it is often the case that a particular application of such types needs not only to inductively generate a collection of objects but also to make identifications between the objects. In classical mathematics one can first generate and then identify, using the Axiom of Choice to lift infinitary constructions to the quotient. HITs can allow one to avoid such non-constructive uses of choice by inter-twining generation and identification. Perhaps more important than the constructive/non-constructive issue is that simultaneously declaring how to generate and how to identify can be a very natural way of defining some construct from the user's point of view. This is why HITs promise to be so useful, once we have robust and convenient mechanisms in theorem-proving systems for defining HITs and defining functions out of HITs. Although some HITs have been axiomatized in various systems, at the moment the only system I know of with built-in support for defining quite general forms of HIT and using them is the implementation of cubical type theory within recent versions of the Agda system.

 

  The higher dimensional aspect of identity in cubical type theory is fascinating; nevertheless, the simpler one-dimensional version of identity, in which one has uniqueness of identity proofs (UIP), is adequate for many applications. Although some regard UIP as a bug of early versions of Agda with it's original form of dependent pattern matching, it is by choice a feature of the Lean prover. Altenkirch and Kaposi have termed the one-dimensional version of HITs quotient inductive types (QITs) and they promise to be very useful even in the setting of type theory with UIP.  In this talk, I survey some of these developments, including a recent reduction of QITs to quotients, and the prospects for better support in theorem-provers for quotient constructions.

 

14:00-14:30Coffee Break
14:30-16:30 Session 8A: Dependent Types and Rewriting. (all times are in CEST timezone - UTC+2)
14:30
Type safety of rewriting rules in dependent types

ABSTRACT. The expressiveness of dependent type theory can be extended by identifying types modulo some additional computation rules. But, for preserving the decidability of type-checking or the logical consistency of the system, one must make sure that those user-defined rewriting rules preserve typing. In this paper, we give a new method to check that property using Knuth-Bendix completion.

15:00
Encoding Agda Programs using Rewriting

ABSTRACT. We present in this paper an encoding in an extension with rewriting of the Edimburgh Logical Framework (LF) [11] of two common features: universe polymorphism and eta-convertibility. This encoding is at the root of the translator between Agda and Dedukti developped by the author.

15:30
The new rewriting engine of Dedukti - System description
PRESENTER: Gabriel Hondet

ABSTRACT. Dedukti is a type-checker for the λΠ-calculus modulo rewriting, an extension of Edinburgh’s Logical Framework (LF) where functions and type symbols can be defined by rewriting rules. It therefore contains an engine for rewriting LF terms and types according to the rewriting rules given by the user. A key component of this engine is the matching algorithm to find which rules can be fired. In this paper, we describe the class of rewriting rules supported by Dedukti and the new implementation of the matching algorithm. Dedukti supports non-linear rewriting rules on terms with binders using higher-order pattern-matching as in Combinatory Reduction Systems (CRS). The new matching algorithm extends the technique of decision trees introduced by Luc Maranget in the OCaml compiler to this more general context.

16:00
A Syntax for Mutual Inductive Families
PRESENTER: Jakob von Raumer

ABSTRACT. Indexed inductive types are a feature of most languages based on dependent types. They are usually described either by syntactic schemes or by encodings of strictly positive functors such as combinator languages or containers. The former approaches are informal and give only external signatures, the latter approaches suffer from encoding overheads and do not directly represent mutual types.

In this paper we propose a direct method for describing signatures for mutual inductive families using a domain-specific type theory. A signature is a context (roughly speaking, a list of types) in this small type theory. Algebras, displayed algebras and sections are defined by models of this type theory: the standard model, the logical predicate and a logical relation interpretation, respectively. We reduce the existence of initial algebras for these signatures to the existence of the syntax of our domain-specific type theory. As this theory is very simple, its normal syntax can be encoded using W-types. To the best of our knowledge, this is the first formalisation of the folklore fact that mutual inductive types can be reduced to indexed W-types.

The contents of this paper were formalised in the proof assistant Agda.

14:30-16:00 Session 8B: Concurrency. (all times are in CEST timezone - UTC+2)
Chair:
14:30
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra

ABSTRACT. Concurrent Kleene Algebra is an elegant tool for equational reasoning about concurrent programs. An important feature of concurrent programs that is missing from CKA is the ability to restrict legal interleavings. To remedy this we extend the standard model of CKA, namely pomsets, with a new feature, called boxes, which can specify that part of the system is protect from outside interference. We study the algebraic properties of this new model. Another drawback of CKA is that the language used for expressing properties of programs is the same as that which is used to express programs themselves. This is often too restrictive for practical purposes. We provide a logic, `pomset logic', that is an assertion language for specifying such properties, and which is interpreted on pomsets with boxes. We develop the basic metatheory for the relationship between pomset logic and CKA, including frame rules to support local reasoning, and illustrate this relationship with simple examples.

15:00
Conditional Bisimilarity for Reactive Systems
PRESENTER: Lars Stoltenow

ABSTRACT. Reactive systems à la Leifer and Milner, an abstract categorical framework for rewriting, provide a suitable framework for deriving bisimulation congruences. This is done by synthesizing interactions with the environment in order to obtain a compositional semantics.

We enrich the notion of reactive systems by conditions on two levels: first, as in earlier work, we consider rules enriched with application conditions and second, we investigate the notion of conditional bisimilarity. Conditional bisimilarity allows us to say that two system states are bisimilar provided that the environment satisfies a given condition.

We present several equivalent definitions of conditional bisimilarity, including one that is useful for concrete proofs and that employs an up-to-context technique, and we compare with related behavioural equivalences. We instantiate reactive systems in order to obtain DPO graph rewriting and consider a case study in this setting.

15:30
Resource-Aware Session Types with Arithmetic Refinements *** Best system description by a junior researcher
PRESENTER: Ankush Das

ABSTRACT. Traditional session types prescribe bidirectional communication protocols for concurrent computations, where well-typed programs are guaranteed to adhere to the protocols. Recent work has extended session types with refinements from linear arithmetic, capturing intrinsic properties of processes and data. These refinements then play a central role in describing sequential and parallel complexity bounds on session-typed programs.

The Rast language and system provide an open-source implementation of session-typed concurrent programs extended with arithmetic refinements as well as ergometric and temporal types to capture work and span of program execution. Type checking relies on Cooper's algorithm for quantifier elimination in Presburger arithmetic with a few significant optimizations, and a heuristic extension to nonlinear constraints. Rast furthermore includes a reconstruction engine so that most program constructs pertaining the layers of refinements and resources are inserted automatically. We provide a variety of examples to demonstrate the expressivity of the language.