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

RDP Programme

RDP 2015 at a glance

June 25-27
Friday-Saturday
June 28
Sunday
June 29
Monday
June 30
Tuesday
July 1
Wednesday
July 2
Thursday
July 3
Friday
  RDP:
9:00
9:15
19:00
RDP:
9:00
14:00
RDP:
9:00
14:00
17:00
20:00
RDP:
9:00
RDP:
9:00
  RTA:
10:45
14:00
16:00
RTA:
10:30
14:00
16:00
RTA:
11:00
  TLCA:
10:30
TLCA:
10:30
14:00
16:00
TLCA:
10:30
14:00
  IFIP:
9:15
10:30
14:00
16:00
  UNIF:
9:00
10:30
14:00
16:30
  HDRA:
9:00
10:30
14:30
16:00
HDRA:
9:15
10:45
14:00
16:00
  HoTT/UF:
10:45
14:00
16:00
HoTT/UF:
10:30
14:00
16:00
  WPTE:
10:30
11:30
14:00
16:30
  HFL:
10:30
  CFAT:
14:00

June 25-27, 2015

PhD Open - Tutorial

Ugo Dal Lago. From Implicit Complexity to Quantitative Resource Analysis

June 28, 2015, Sunday

UNIF 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 "signal-flow diagrams" to describe processes where real-valued 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 finite-dimensional 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 signal-flow diagrams also includes "caps" and "cups" to model feedback. This amounts to working with a larger symmetric monoidal category where objects are still finite-dimensional 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 dagger-Frobenius 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 Non-Orientable 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 non-orientable equations, and report on development of a ground confluence prover.

Coffee break (10:00-10:30)

IFIP Second Morning Session

  1. 10:30: Gilles Dowek. Polarization and Reachability
  2. 11:15: Stéphane Graham-Lengrand. Non-idempotent Intersection Types and Quantitative Information about Reduction Paths: A Survey
    Abstract:
    Over the recent years, a new area in the study of intersection types has been explored. In the original spirit of intersection types, a term is of type A /\ B if it is both of type A and of type B, which naturally leads to an idempotent view of intersections: A /\ A is the same type as A. Dropping this idempotency property of intersections allows the design of resource-aware type systems, with deep connections to linear logic. This enriches typing with quantitative information about the lengths of reduction paths from typed terms. Upper bounds for these lengths -or even sometimes exact characterisations- have been provided by such typing systems, for various abstract machines and reduction strategies in the lambda-calculus and some of its variants. Among these, explicit substitution calculi proved a particularly appropriate approach to establishing such results. We will review this line of research, where typing is brought much closer to operational and denotational semantics, and discuss the connections that it opened towards neighbouring areas.
  3. 12:00: Discussion on ISR (discussion chair: Aart Middeldorp): - Report on ISR'15 (Johannes Waldmann), - Report on ISR'16 (Mauricio Ayala-Rincón), - Report/Propsals for ISR'17 (Mauricio Ayala-Rincón)

UNIF Second Morning Session

  1. 10:30: Tomer Libal. Towards Deciding Second-order Unification Problems Using Regular Tree Automata
  2. 11:00: Vincent Van Oostrom, Femke Van Raamsdonk. Matching in the Dynamic Pattern Calculus
  3. 11:30: Franz Baader, Pierre Ludmann. The Exact Unification Type of Commutative Theories
  4. 12:00: Franz Baader, Stefan Borgwardt, Barbara Morawska. Dismatching and Local Disunification in EL

HDRA Morning Session

  1. 10:30: Jovana Obradović. The Bénabou-Roubaud Monadic Descent Theorem via String Diagrams
  2. 11:15: Short break
  3. 11:30: Jason Morton, David Spivak. An Operad-based Normal Form for Morphism Expressions in a Closed Compact Category

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:30-14:00)

IFIP First Afternoon Session

  1. 14:00: Luke Ong. Compositional Higher-Order Model Checking, and the Model Checking of Higher-type Böhm Trees
  2. 14:45: Discussion on IFIP (discussion chair: Ugo Dal Lago): - Modernisation of aims, - Stand-alone events

UNIF Invited Talk and First Afternoon Session

  1. 14:00: Maribel Fernandez. Nominal Equational Unification (Invited Talk)
  2. 15:00: Ana Cristina Rocha-Oliveira, Mauricio Ayala-Rincon, Maribel Fernandez. Formalising the Completeness of a Nominal Unification Algorithm
  3. 15:30: Giovanni Bernardi, Simon Gay, Vasco T. Vasconcelos. Unification of Session Trees

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:30-16:00)

IFIP Second Afternoon Session

  1. 16:00: Kris Rose. Proposal Joint Conference RTA/TLCA
  2. 16:30: Discussion on Future of RTA/TLCA (discussion chair: Georg Moser): - FSCD Proposal
  3. 17:15: Business Meeting

HDRA Afternoon Session

  1. 16:00: Krzysztof Bar, Jamie Vicary, Aleks Kissinger. Globular: a Proof Assistant for Semistrict Higher Rewriting
  2. 16:45: Short break
  3. 17:00: Eric Finster. Opetopic Diagrams and Higher Categorical Proof Theory

UNIF Second Afternoon Session

  1. 16:30: Serdar Erbatur, Kimberly A. Gero, Andrew M. Marshall, Catherine Meadows, Paliath Narendran. Unification modulo a Theory of Pairing Encryption
  2. 17:00: Munehiro Iwami. Uniform Semi-Unification and Anchored Semi-Unification
  3. 17:30: Business Meeting

June 29, 2015, Monday

RDP Opening

RTA Invited Talk (chair: Horatiu Cirstea)

9:15: Grigore Roşu. Matching Logic (slides, PPTX)

Abstract:
Matching logic is a first-order 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 power-set 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 off-the-shelf provers and SMT solvers can be used for matching logic reasoning. Matching logic is particularly well-suited for reasoning about programs in programming languages that have a rewrite-based operational semantics.

HDRA Invited Talk

9:15: Eugenia Cheng. Distibutive Laws for Lawvere Theories (II)

Coffee break (10:15-10:45)

RTA Morning Session – Termination and Strategies (chair: Georg Moser)

  1. 10:45: David Sabel, Hans Zantema. Transforming Cycle Rewriting into String Rewriting
  2. 11:15: Horatiu Cirstea, Serguei Lenglet, Pierre-Etienne Moreau. A Faithful Encoding of Programmable Strategies into Term Rewriting Systems
  3. 11:45: Thomas Genet, Yann Salmon. Reachability Analysis of Innermost Rewriting
  4. 12:15: Joerg Endrullis, Hans Zantema. Proving Non-termination by Finite Automata

HDRA Morning Session

  1. 10:45: Cyrille Chenavier. Confluence Algebras and Acyclicity of the Koszul Complex
  2. 11:30: Short break
  3. 11:45: Clément Alleaume. Rewriting in the Category of Bott-Samelson Bimodules

HoTT/UF Morning Session (Coq for HoTT)

  1. 10:45: Mathieu Sozeau. Coq Support for HoTT (Invited Talk)
    Abstract:
    In this tutorial I will present up-and-coming, definitional extensions for the development of HoTT in Coq. The first, a generalized rewriting framework working in Type, enables rewriting with equivalences, relevant identity or any user defined relevant rewriting relation in any context. The second, a work-in-progress update of the Equations package, enables full dependent pattern-matching syntax for writing programs, using general well-founded recursion and making use of the h-level information on types to compile pattern-matching down to pure, axiom-free Coq terms. It also provides tools to reason on programs after the fact without leaking details of the elaboration. In particular it derives powerful functional elimination principles coming from the the inductively defined graphs of functions. We will discuss potential applications and extensions with HITs. This is joint work with Cyprien Mangin.
  2. 11:45: Assia Mahboubi. Coq Libraries for HoTT (Invited Talk)
    Abstract:
    Many investigations in Homotopy Type Theory and Univalent Foundations have been simultaneously formalized and machine-checked in pre-existing (like Agda or Coq) or new (like Lean) proof assistants, possibly customized for this purpose. This results today in rather larger corpus of formal libraries, that require some care and maintenance from their authors in order to remain a robust and extensible socle for further developments. In this lecture we do not present new formalized results but rather try to illustrate how the techniques drawn up in the collaborative development of large libraries like the Mathematical Components can apply to this flavor of formalizations.

Lunch break (12:45-14:00)

RTA First Afternoon Session – Algebra and Equational Reasoning (chair: Kristoffer Rose)

  1. 14:00: Lars Hellström. Network Rewriting II: Bi- and Hopf Algebras
  2. 14:30: Anupam Das, Lutz Strassburger. No Complete Linear Term Rewriting System for Propositional Logic
  3. 15:00: Joerg Endrullis, Helle Hvid Hansen, Dimitri Hendriks, Andrew Polonsky, Alexandra Silva. A Coinductive Framework for Infinitary Rewriting and Equational Reasoning (RTA Best Paper)

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 finite-dimensional 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)

  1. 14:00: Simon Huber, Cyril Cohen, Thierry Coquand, Anders Mörtberg. A Cubical Type Theory
  2. 14:45: Round table

Coffee break (15:30-16:00)

RTA Second Afternoon Session – Unification (chair: Mauricio Ayala Rincón)

  1. 16:00: Franz Baader, Stefan Borgwardt, Barbara Morawska. Dismatching and Local Disunification in EL
  2. 16:30: Ilias Kotsireas, Temur Kutsia, Dimitris E. Simos. Constructing Orthogonal Designs in Powers of Two: Groebner Bases Meet Equational Unification
  3. 17:00: Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret. Nominal Anti-Unification

HDRA Second Afternoon Session

  1. 16:00: Lucius Meredith, Mike Stay. Higher Category Models of the π-Calculus
  2. 16:45: Short break
  3. 17:00: Aleks Kissinger, Jamie Vicary. Semistrict n-Categories via Rewriting

HoTT/UF Second Afternoon Session (Sheaves in HoTT)

  1. 16:00: Hugo Herbelin. An Inductive Dependently-Typed Construction of Simplicial Sets and of Similar Presheaves over a Reedy Category
  2. 16:30: Kevin Quirin. Lawvere-Tierney Sheafification in Homotopy Type Theory
  3. 17:00: Andreas Nuyts, Jesper Cockx, Dominique Devriese, Frank Piessens. Towards a Directed HoTT with Four Kinds of Variance

Welcome Reception

June 30, 2015, Tuesday

RTA 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 cyber-physical 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 well-suited 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 model-checking. 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

  • Analysis of engineered systems
    • finding problems and fixing the system,
    • optimizing performance.
  • Analysis of natural systems
    • finding problems and fixing the model,
    • using the model to predict consequences of perturbations.

To be self-contained, the talk will begin with a little introduction to RWL and Maude.

Coffee break (10:00-10:30)

RTA Morning Session – Complexity and Strategies (chair: Jürgen Giesl)

  1. 10:30: Johannes Waldmann. Matrix Interpretations on Polyhedral Domains
  2. 11:00: Martin Avanzini, Christian Sternagel, René Thiemann. Certification of Complexity Proofs using CeTA
  3. 11:30: Cynthia Kop, Aart Middeldorp, Thomas Sternagel. Conditional Complexity
  4. 12:00: Nao Hirokawa, Aart Middeldorp, Georg Moser. Leftmost Outermost Revisited

HoTT/UF Morning Session (Univalence)

  1. 10:30: Thorsten Altenkirch. Univalence for Dummies? (Invited Talk)
    Abstract:
    One of the central principles of Homotopy Type Theory is the univalence "axiom" which basically states that equivalent types are equal. But why is this sound? Both the setoid model and the groupoid model give us a limited form of univalence but how to scale it up? Are Kan complexes the right answer? Or cubical sets? I would like to discuss this question and I expect some useful input from the audience.
  2. 11:30: Christian Sattler. Ordinary and Indexed W-Types
  3. 12:00: Nicolai Kraus. Eliminating out of Truncations

Lunch break (12:30-14:00)

RDP Plenary Session and First RTA Afternoon Session

  1. 14:00: Vladimir Voevodsky. From Syntax to Semantics of Dependent Type Theories — Formalized (slides, PDF)
    Abstract:
    The keystone of the homotopy type theory and univalent foundations is the interpretation of the Calculus of Inductive Constructions into Kan simplicial sets that satisfies the univalence axiom. The detailed description of this interpretation is very complex and requires new level of generality and precision in the theory of syntax and semantics of dependent type theories. I will report on the current state of the program for a rigorous, formalizable approach to the construction of models of complex dependent type theories that I have been working on since 2009.
  2. 15:00: Florence Clerc, Samuel Mimram. Presenting Categories Modulo a Rewriting System

Coffee break (15:30-16:00)

RTA Second Afternoon Session – System Descriptions (chair: Femke van Raamsdonk)

  1. 16:00: Florian Frohn, Jürgen Giesl, Jera Hensel, Cornelius Aschermann, Thomas Stroeder. Inferring Lower Bounds for Runtime Complexity
  2. 16:30: Markus Lepper, Baltasar Trancón Y Widemann. A Simple and Efficient Step Towards Type-Correct XSLT Transformations
  3. 17:00: Vlad Vergu, Pierre Neron, Eelco Visser. DynSem: A DSL for Dynamic Semantics Specification based on Implicitly Modular Reduction Rules

HoTT/UF First Afternoon Session (Modelling Types)

  1. 16:00: Benedikt Ahrens. Models of Type Theory in Univalent Mathematics (Invited Talk)
    Abstract:
    The categorical semantics of type theory has been subject of research since the 1970s. A model of type theory is usually defined to be a category - modelling contexts and their morphisms - that is equipped with additional structure accounting for types and terms, and operations such as substitution. The type theory itself can be given such a structure of a model - in fact, the inductive structure of type theory entails that it is the initial such model in a suitable sense. Various definitions of models as "categories with extra structure" have been studied, amongst them - categories with families ; - categories with attributes ; - categories with display maps ; - comprehension categories. In a set-theoretic setting, the relationship between those concepts is well-known. In ongoing work with Peter LeFanu Lumsdaine and Vladimir Voevodsky, we try to understand the relation between these different notions in univalent mathematics, by exhibiting maps between the different types of such models and showing which are embeddings, equivalences, and so on. In this talk I will give an overview of the UniMath library, a library of univalent mathematics formalized using the proof assistant Coq, and of our formalization of models of type theory based on the UniMath library.
  2. 17:00: Martin Escardo, Thierry Coquand. The Geometry of Constancy
  3. 17:30: Discussion

July 1, 2015, Wednesday

RTA 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:00-10:30)

TLCA Morning Session – Homotopy Type Theory (chair: Peter LeFanu Lumsdaine)

  1. 10:30: Marc Bezem, Thierry Coquand, Erik Parmann. Non-Constructivity in Kan Simplicial Sets
  2. 11:00: Benedikt Ahrens, Paolo Capriotti, Régis Spadotti. Non-Wellfounded Trees in Homotopy Type Theory
  3. 11:30: Elliot Fairweather, Maribel Fernández, Nora Szasz, Alvaro Tasistro. Dependent Types for Nominal Terms with Atom Substitutions
  4. 12:00: André Hirschowitz, Tom Hirschowitz, Nicolas Tabareau. Wild ω-Categories for the Homotopy Hypothesis in Type Theory

RTA Morning Session – Confluence (chair: Temur Kutsia)

  1. 10:30: Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama. Confluence of Orthogonal Nominal Rewriting Systems Revisited
  2. 11:00: Łukasz Czajka. Confluence of Nearly Orthogonal Infinitary Term Rewriting Systems
  3. 11:30: Julian Nagele, Bertram Felgenhauer, Aart Middeldorp. Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules
  4. 12:00: Julian Nagele, Harald Zankl. Certified Rule Labeling

Lunch break (12:30-14: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, Thursday

TLCA 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 well-known 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 call-by-value and call-by-name.

Coffee break (10:00-10:30)

TLCA Morning Session – Rewriting in Type Theory (chair: Herman Geuvers)

  1. 10:30: Martin Hofmann, Georg Moser. Multivariate Analysis
  2. 11:00: Jean-Pierre Jouannaud, Jian-Qi Li. Termination of Dependently Typed Rewrite Rules
  3. 11:30: Ali Assaf. Conservativity of Embeddings in the λΠ Calculus Modulo Rewriting
  4. 12:00: Gabriel Scherer. Multi-Focusing on Extensional Rewriting with Sums

WPTE Opening and Invited Talk (chair: Naoki Nishida)

10:30: Brigitte Pientka. Mechanizing Meta-Theory 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 first-class contexts to abstract over a set of assumptions, contextual objects to model derivations that depend on assumptions, and first-class 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 Curry-Howard isomorphism. Recently, the Beluga system has also been extended with a totality checker which guarantees that recursive programs are well-founded 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 Schmidt-Schauß)

  1. 11:30: Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama. Context-Moving Transformation for Term Rewriting Systems
  2. 12:00: Adrián Palacios, Germán Vidal. Towards Modelling Actor-Based Concurrency in Term Rewriting

Lunch break (12:30-14:00)

TLCA First Afternoon Session – Proof Theory (chair: Jean-Pierre Jouannaud)

  1. 14:00: Giulio Guerrieri, Luca Paolini, Simona Ronchi Della Rocca. Standardization of a Call-By-Value Lambda-Calculus
  2. 14:30: Martin Escardo, Chuangjie Xu. The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation
  3. 15:00: Bahareh Afshari, Stefan Hetzl, Graham Leigh. Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars
  4. 15:30: José Espírito Santo. Curry-Howard for Sequent Calculus at Last!

WPTE First Afternoon Session (chair: Yuki Chiba)

  1. 14:00: Naosuke Matsuda. A Simple Extension of the Curry-Howard Correspondence with Intuitionistic Lambda Rho Calculus
  2. 14:30: Sjaak Smetsers, Ken Madlener, Marko Van Eekelen. Formalizing Bialgebraic Semantics in PVS 6.0
  3. 15:00: David Sabel, Manfred Schmidt-Schauß. Observing Success in the Pi-Calculus
  4. 15:30: Giulio Guerrieri. Head Reduction and Normalization in a Call-by-Value Lambda-Calculus

Coffee break (16:00-16:30)

TLCA Second Afternoon Session – Contexts and Types (chair: Matthieu Sozeau)

  1. 16:30: Antonio Bucciarelli, Delia Kesner, Simona Ronchi Della Rocca. Observability for Pair Pattern Calculi
  2. 17:00: Brigitte Pientka, Andreas Abel. Well-Founded Recursion over Contextual Objects
  3. 17:30: Yuting Wang, Kaustuv Chaudhuri. A Proof-theoretic Characterization of Independence in Type Theory

WPTE Second Afternoon Session (chair: Santiago Escobar)

  1. 16:30: Guillaume Madelaine, Cédric Lhoussaine, Joachim Niehren. Structural Simplification of Chemical Reaction Networks Preserving Deterministic Semantics
  2. 17:00: Business Meeting and Closing

July 3, 2015, Friday

TLCA 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 Martin-Lö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:00-10:30)

TLCA Morning session – Category Theory (chair: Benedikt Ahrens)

  1. 10:30: Robert Atkey, Neil Ghani, Fredrik Nordvall Forsberg, Timothy Revell, Sam Staton. Models for Polymorphism over Physical Dimensions
  2. 11:00: Simon Castellan, Pierre Clairambault, Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category
  3. 11:30: Jonas Frey. Realizability Toposes from Specifications
  4. 12:00: Colin Riba. Fibrations of Tree Automata

Lunch break (12:30-14:00)

TLCA Afternoon Session – Types and Surprises (chair: Damian Niwiński)

  1. 14:00: Marc Bagnol. MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams
  2. 14:30: Brian Redmond. Polynomial Time in the Parametric Lambda Calculus
  3. 15:00: Dariusz Biernacki, Piotr Polesiuk. Logical Relations for Coherence of Effect Subtyping
  4. 15:30: Jan Bessai, Andrej Dudenhefner, Boris Duedder, Ugo De'Liguoro, Tzu-Chun Chen, Jakob Rehof. Mixin Composition Synthesis Based on Intersection Types








Important information

Plenary speakers

Google+
Valid XHTML 1.1 Valid CSS!