Abstract. We study the notion of backreference in practical regular expressions with the purpose of formal analysis and theorem proving. So far only their operational semantics was studied in formal language theory. However, for efficient reasoning and independence from implementations we need a mathematical concept of backreference that does not depend on evaluation strategies, etc. We introduce such a notion in terms of a possibly infinite set of finite tree unfoldings of regular expressions for which we state the finiteness of a partial derivative (actually, prebase) representation.

Abstract. We study a derivative method allowing to prove termination of computations on regular expressions. A Coq formalisation of a canonical non-deterministic finite automaton construction on a regular expression is presented. The correctness of the functional definitions is formally verified in Coq using the libraries and the small-scale reflection tools of Ssreflect. We propose to extend the proofs further, and this is a work in progress, to study termination of containment and equivalence in terms of partial derivatives. This serves as a major motivation and intended application of the presented approach. A method that we develop in the paper, called shadowing, allows for a smooth program extraction from decision procedures whatever the complexity of the dependently typed proofs.

Abstract. In this paper we show that a prototypical subtype relation that can neither be defined as a least fixed point nor as a greatest fixed point can nevertheless be defined in a dependently typed language with inductive and coinductive types. The definition proceeds alike a fold in functional programming, although a rather unusual one: that is not applied to any starting object. There has been a related construction of bisimilarity in Coq by Nakata and Uustalu recently, however, our case is not concerned with bisimilarity but a weaker notion of similarity that corresponds to recursive subtyping and has it's own interesting problems.

Abstract. We propose a technique of packed view for interactive communication between heterogeneous software such as theorem provers and computer algebra systems. A packed view is a method to infer, with a possible share of user interaction, the type-theoretic meaning of a given pre-structured object, as well as a method to display the underlying syntactic structure of a semantic term as a pre-structured object (essentially, an abstract syntax tree) corresponding to it. With this notion of view in hand, it is relatively straightforward to program non-trivial parts of communication interfaces between a theorem prover and a computer algebra using the logic of the prover as the programming language.

Abstract. Regular expression containment has recently enjoyed a renewed interest as a type-theoretic problem. By viewing regular expressions as types, it is possible to view containments as functions that coerce one regular expression into another. Containment of a given regular expression in another one is therefore a coercion inference problem. It is not straightforward how to apply here generic proof-theoretic approaches such as those based on the MALL with the least fixpoint. We propose an alternative approach, still a purely syntactic one, to decide containment in reasonable time. We employ the partial derivative construction that, for a regular expression E, yields a syntactic NFA recognising the language of E; and, for a containment E ≤ F, it yields a simulation of E by F, with the empty simulation representing the absence of coercion. We are currently working on a proof of completeness of this optimised coercion search algorithm.

Abstract. In this paper, we present a computer-checked, constructive soundness and completeness result for prototypic recursive type containment with respect to containment of non-wellfounded (finite or infinite) trees. The central role is played by formalisation of substitution of recursive types as a monad, with a traverse function implementing a strategy for potentially infinite recursive unfolding. In the rigorous setting of constructive type theory, the very definition of subtyping should be scrutinised to allow a prover to accept it. As a solution, we adapt the method of weak bisimilarity by mixed induction-coinduction recently introduced to Coq by Nakata and Uustalu. However, our setting is different in that we work with a notion of weak similarity that corresponds to subtyping. We accomplish the task of representing infinitary subtyping in the Calculus of (Co-)Inductive Constructions. Our technique does not require extensions of the Calculus and therefore can be ported to other dependently typed languages.

(Superseded by the extended post-proceedings version.)