Session 8A

Chair: Sandra Alves

• 14:30: Frédéric Blanqui. Type safety of rewriting rules in dependent types.     See abstract ...
  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: Guillaume Genestier. Encoding Agda Programs using Rewriting.     See abstract ...
  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: Gabriel Hondet, Frédéric Blanqui. The new rewriting engine of Dedukti - System description.     See abstract ...
  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: Ambrus Kaposi, Jakob von Raumer. A Syntax for Mutual Inductive Families.     See abstract ...
  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.