International Conference on Rewriting, Deduction, and Programming June 29 to July 3, 2015 Warsaw, Poland 


RDP ProgrammeRDP 2015 at a glance
June 2527, 2015PhD Open  Tutorial Ugo Dal Lago. From Implicit Complexity to Quantitative Resource Analysis June 28, 2015, SundayUNIF Invited Talk 9:00: Artur Jeż. Deciding Context Unification HDRA Invited Talk 9:00: John Baez. Categories in Control
Abstract:
Control theory is the branch of engineering that studies dynamical systems with inputs and outputs, and seeks to stabilize these using feedback. Control theory uses "signalflow diagrams" to describe processes where realvalued functions of time are added, multiplied by scalars, differentiated and integrated, duplicated and deleted. In fact, these are string diagrams for the symmetric monoidal category of finitedimensional vector spaces, but where the monoidal structure is direct sum rather than the usual tensor product. Jason Erbele has given a presentation for this symmetric monoidal category, which amounts to saying that it is the PROP for bicommutative bimonoids with some extra structure. A broader class of signalflow diagrams also includes "caps" and "cups" to model feedback. This amounts to working with a larger symmetric monoidal category where objects are still finitedimensional vector spaces but the morphisms are linear relations. Erbele also found a presentation for this larger symmetric monoidal category. It is the PROP for a remarkable thing: roughly speaking, an object with two special commutative daggerFrobenius structures, such that the multiplication and unit of either one and the comultiplication and counit of the other fit together to form a bimonoid. IFIP First Morning Session 9:15: Takahito Aoto. Proving Ground Confluence of Term Rewriting Systems by Rewriting Induction with NonOrientable Equations
Abstract:
Ground confluence of term rewriting systems guarantees that all ground terms are confluent. Not confluence but ground confluence often matters in applications where not the equational validity but the inductive validity is of concern. Recently, interests for proving confluence of term rewriting systems automatically have been grown, and confluence provers have been developed. In contrast, it seems that little interests have been paid on developing tools for proving ground confluence automatically. In this talk, present a theoretically simple approach for proving ground confluence of term rewriting systems based on rewriting induction with nonorientable equations, and report on development of a ground confluence prover.
Coffee break (10:0010:30) IFIP Second Morning Session
UNIF Second Morning Session
HDRA Morning Session
HFL Tutorial 10:30: Krzysztof Ziemiański. Homotopy for Laymen
Abstract:
Homotopy Type Theory is a very dynamically growing branch of the study within the type theory. Understanding its dynamics requires good knowledge of both type theory and topology. To bring the developments closer to a wider audience within community of people who study types, we propose a quick introduction to the basic notions of homotopy theory with necessary geometrical insights and suggestion of how combinatorial structures appearing in homotopy theory can be exploited for type theoretical considerations.
Lunch break (12:3014:00) IFIP First Afternoon Session
UNIF Invited Talk and First Afternoon Session
CFAT Tutorial 14:00: Jacek Chrząszcz. Coq for Algebraic Topologists
Abstract:
An important advantage of systems such as Coq is that they make it possible to manage complicated proof structures. As a result, it becomes possible to do reliable proofs for mathematical models that are bigger than so far employed. This is evidenced by successful developments of formal proofs for the Four Colour Theorem and Odd Order Theorem  both being theorems that brought many doubts about the correctness of the final argument. These doubts arised because those proofs were clearly on the verge of efficiency for traditional paper and pencil mathematical methods.
Currently, the mathematical models used in algebraic topology become more and more sophisticated, which creates potential to apply proof assistants in the field. A short course of Coq will be presented on the content that comes from the algebra to show the potential of Coq in analysis of algebraic models. HDRA Invited Talk 14:30: Eugenia Cheng. Distibutive Laws for Lawvere Theories (I) Coffee break (15:3016:00) IFIP Second Afternoon Session
HDRA Afternoon Session
UNIF Second Afternoon Session
June 29, 2015, MondayRDP Opening RTA Invited Talk (chair: Horatiu Cirstea) 9:15: Grigore Roşu. Matching Logic (slides, PPTX)
Abstract:
Matching logic is a firstorder logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching.
Its sentences, the patterns, are constructed using
variables, symbols, connectives and quantifiers,
but no difference is made between function and predicate symbols.
In models, a pattern evaluates into a powerset domain (the set of values
that match it), in contrast to FOL where functions and predicates
map into a regular domain.
Matching logic uniformly generalizes several logical frameworks important
for program analysis, such as: propositional logic, algebraic specification,
FOL with equality, and separation logic.
Patterns can specify separation requirements at any level
in any program configuration, not only in the heaps or stores, without
any special logical constructs for that: the very nature of pattern
matching is that if two structures are matched as part of a pattern, then
they can only be spatially separated.
Like FOL, matching logic can also be translated into pure predicate logic,
at the same time admitting its own sound and complete proof system.
A practical aspect of matching logic is that FOL reasoning remains sound,
so offtheshelf provers and SMT solvers can be used for matching logic
reasoning.
Matching logic is particularly wellsuited for reasoning about programs
in programming languages that have a rewritebased operational semantics.
HDRA Invited Talk 9:15: Eugenia Cheng. Distibutive Laws for Lawvere Theories (II) Coffee break (10:1510:45) RTA Morning Session – Termination and Strategies (chair: Georg Moser)
HDRA Morning Session
HoTT/UF Morning Session (Coq for HoTT)
Lunch break (12:4514:00) RTA First Afternoon Session – Algebra and Equational Reasoning (chair: Kristoffer Rose)
HDRA Invited Talk 14:30: John Baez. Circuits, Categories, and Rewrite Rules
Abstract:
We describe a category where a morphism is an electrical circuit made of resistors, inductors and capacitors, with marked input and output terminals. In this category we compose morphisms by attaching the outputs of one circuit to the inputs of another. There is a functor called the "black box functor" that takes a circuit, forgets its internal structure, and remembers only its external behavior. Two circuits have the same external behavior if and only if they impose same relation between currents and potentials at their terminals. This is a linear relation, so the black box functor goes from the category of circuits to the category of finitedimensional vector spaces and linear relations. Constructing this functor makes use of Brendan Fong's theory of "decorated cospans" – and the question of whether two circuits map to the same relation has an interesting answer in terms of rewrite rules.
HoTT/UF First Afternoon Session (Cubical Sets)
Coffee break (15:3016:00) RTA Second Afternoon Session – Unification (chair: Mauricio Ayala Rincón)
HDRA Second Afternoon Session
HoTT/UF Second Afternoon Session (Sheaves in HoTT)
Welcome Reception June 30, 2015, TuesdayRTA Invited Talk (chair: Maribel Fernández) 9:00: Carolyn Talcott. Executable Formal Models in Rewriting Logic (slides, PDF)
Abstract:
Formal executable models provide a means to gain insights into the behavior of complex distributed systems. Ideas can be prototyped and assurance gained by carrying out analyses at different levels of fidelity: searching for desirable or undesirable behaviors, determining effects of perturbing the system, and eventually investing effort to carry out formal proofs of key properties. This modeling approach applies to a wide range of systems, including a variety of protocols and networked cyberphysical systems. It is also emerging as an important tool in understanding many different aspects of biological systems. Rewriting logic (RWL) is a formalism that is wellsuited to developing and working with formal executable models. In RWL term rewriting is used to represent both structure (equational properties and functions) and transformation / behavior. Logics and inference systems can be naturally represented in RWL, as can the structure and behavior of distributed systems both engineered and natural. Maude is a high performance realization of Rewriting Logic. Maude specifications are naturally executable and the Maude environment provides a variety analysis tools to reason about properties of models. These include reachability analysis, symbolic execution (narrowing), and modelchecking. In addition, Maude is reflective. This provides a powerful mechanism for extension. The talk will present a sampling of executable specifications using Maude and its extensions. The examples will illustrate a range of modeling problems and analysis approaches, including
To be selfcontained, the talk will begin with a little introduction to RWL and Maude. Coffee break (10:0010:30) RTA Morning Session – Complexity and Strategies (chair: Jürgen Giesl)
HoTT/UF Morning Session (Univalence)
Lunch break (12:3014:00) RDP Plenary Session and First RTA Afternoon Session
Coffee break (15:3016:00) RTA Second Afternoon Session – System Descriptions (chair: Femke van Raamsdonk)
HoTT/UF First Afternoon Session (Modelling Types)
July 1, 2015, WednesdayRTA and TLCA Invited Talk (chair: Maribel Fernández and Thorsten Altenkirch) 9:00: Hélène Kirchner. Port Graphs, Rules and Strategies for Dynamic Data Analytics (slides, PDF)
Abstract:
In the context of understanding, planning and anticipating the behaviour of complex systems, such as biological networks or social networks, this talk proposes port graphs, rules and strategies, combined in strategic rewrite programs, as foundational ingredients for interactive and visual programming and shows how they can contribute to dynamic data analytics.
Coffee break (10:0010:30) TLCA Morning Session – Homotopy Type Theory (chair: Peter LeFanu Lumsdaine)
RTA Morning Session – Confluence (chair: Temur Kutsia)
Lunch break (12:3014:00) Business Meeting 14:00: (1) Report from the organizers and from RTA and TLCA PC. (2) RTA Test of Time Award. (3) Proposal of the new conference FSCD. (4) Announcement of the conference in 2016. (6) Proposals for 2017. Visit to a Museum 17:00: The Museum of the History of Polish Jews admits participants between 5 and 6 p.m. Social Dinner 20:00: The dinner is served in the restaurant of the Museum. July 2, 2015, ThursdayTLCA Invited Talk (chair: Gilles Dowek) 9:00: Herman Geuvers. Inductive and Coinductive Data Types in Typed Lambda Calculus Revisited (slides, PDF)
Abstract:
In lambda calculus there are various ways to represent data, of which the Church encoding is the most wellknown one. The Scott encoding is another one, which has gained new interest, among others from researchers in implicit computational complexity. Combining the Church and Scott encoding, one gets the recursive encoding, or Parigot encoding which has advantages over the other two in terms of representability of functions. In the talk we will give an overview of the various approaches to data types in lambda calculus, how they can be typed, how one can extract programs from proof and what the specific pros and cons are. We will show to what extent these approaches can be dualized to the coinductive case. Then we will present a calculus where Scott data types can be used to combine callbyvalue and callbyname. Coffee break (10:0010:30) TLCA Morning Session – Rewriting in Type Theory (chair: Herman Geuvers)
WPTE Opening and Invited Talk (chair: Naoki Nishida) 10:30: Brigitte Pientka. Mechanizing MetaTheory in Beluga
Abstract:
Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will survey the proof environment Beluga. To specify formal systems and represent derivations within them, Beluga provides a sophisticated infrastructure based on the logical framework LF; in particular, its infrastructure not only supports modelling binders via binders in LF, but extends and generalizes LF with firstclass contexts to abstract over a set of assumptions, contextual objects to model derivations that depend on assumptions, and firstclass simultaneous substitutions to relate contexts. These extensions allow us to directly support key and common concepts that frequently arise when describing formal systems and derivations within them.
To reason about formal systems, Beluga provides a dependently typed functional language for implementing inductive proofs about derivations as recursive functions on contextual objects following the CurryHoward isomorphism. Recently, the Beluga system has also been extended with a totality checker which guarantees that recursive programs are wellfounded and correspond to inductive proofs and an interactive program development environment to support incremental proof / program construction.
Taken together these extensions enable direct and compact mechanizations. To demonstrate Beluga's strength, we develop a weak normalization proof using logical relations.
WPTE Morning Session (chair: Manfred SchmidtSchauß)
Lunch break (12:3014:00) TLCA First Afternoon Session – Proof Theory (chair: JeanPierre Jouannaud)
WPTE First Afternoon Session (chair: Yuki Chiba)
Coffee break (16:0016:30) TLCA Second Afternoon Session – Contexts and Types (chair: Matthieu Sozeau)
WPTE Second Afternoon Session (chair: Santiago Escobar)
July 3, 2015, FridayTLCA Invited Talk (chair: Peter Dybjer) 9:00: Martin Hofmann. The Groupoid Interpretation of Type Theory, a Personal Retrospective (slides, PDF)
Abstract:
Back in 1994 Thomas Streicher and myself discovered the groupoid
interpretation of MartinLöf's type theory which is now seen as a
precursor of Homotopy Type Theory and in fact anticipated some simple
cases of important ideas of Homotopy Type Theory, notably a special case
of the univalence axiom. I will explain how and why we found the
groupoid interpretation, our motivations and results. I will also try to
give an informed outsider's view of Homotopy Type Theory as it is today
and finally give a glance at a novel application of the groupoid
interpretation in the context of denotational semantics ("proof relevant
logical relations").
Coffee break (10:0010:30) TLCA Morning session – Category Theory (chair: Benedikt Ahrens)
Lunch break (12:3014:00) TLCA Afternoon Session – Types and Surprises (chair: Damian Niwiński)
