The aim of WPTE is to bring together the researchers working on program transformations, evaluation, and operationally-based programming language semantics, using rewriting methods, in order to share the techniques and recent developments and to exchange ideas to encourage further activation of research in this area. The previous WPTE was held in Vienna 2014.
Topics of interest in the scope of this workshop include:
Program transformation and evaluation for Haskell and Rewriting is a new topic of this workshop: equational reasoning and other rewriting techniques for program verification and analysis; lambda calculi and type systems for functional programs and higher-order rewrite systems; rewriting of type expressions in the type checker; rewriting of programs by refactoring tools, optimizers, code generators; execution of programs as a form of graph rewriting (terms with sharing); Template Haskell, generally introducing a rewriting-like macro language into the compilation process; rewriting modulo commonly occurring axioms such as associativity, commutativity, and identity element.
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.
- 09:00-10:00
- (TLCA Invited Talk)
- Note that participants of WPTE can attend the invited talk of TLCA.
- 10:00-10:30
- Coffee break
- 10:30-11:30 Opening and Invited Talk (chair: N. Nishida)
- Mechanizing Meta-Theory in Beluga
Brigitte Pientka- 11:30-12:30 Session 1 (chair: M. Schmidt-Schauß)
- Context-Moving Transformation for Term Rewriting Systems
Koichi Sato, Kentaro Kikuchi, Takahito Aoto, and Yoshihito Toyama- Towards Modelling Actor-Based Concurrency in Term Rewriting
Adrián Palacios and Germán Vidal- 12:30-14:00
- Lunch
- 14:00-16:00 Session 2 (chair: Y. Chiba)
- A Simple Extension of the Curry-Howard Correspondence with Intuitionistic Lambda Rho Calculus
Naosuke Matsuda- Formalizing Bialgebraic Semantics in PVS 6.0
Sjaak Smetsers, Ken Madlener, and Marko Van Eekelen- Observing Success in the Pi-Calculus
David Sabel and Manfred Schmidt-Schauß- Head Reduction and Normalization in a Call-by-Value Lambda-Calculus
Giulio Guerrieri- 16:00-16:30
- Coffee break
- 16:30-17:00 Session 3 (chair: S. Escobar)
- Structural Simplification of Chemical Reaction Networks Preserving Deterministic Semantics
Guillaume Madelaine, Cédric Lhoussaine, and Joachim Niehren- 17:00-17:30 Business Meeting and Closing
- Business Meeting
- Closing
See also the program of RDP 2015.
The OASIcs proceedings are available via http://www.dagstuhl.de/dagpub/978-3-939897-94-1. New!
Y. Chiba, S. Escobar, N. Nishida, D. Sabel, and M. Schmidt-Schauß (Eds.)
2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation
OASICS Vol. 46, Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2014
Extended abstracts on work in progress are not included in the OASIcs proceedings but they will be included in the USB memory which is distributed to the RDP partipicants.
Registration is via the RDP 2015 registration system.
Note that the early registration deadline ends on May 22!
The call for papers is available in TXT-format.
WPTE accepts two different kinds of contributions:
One author of each accepted paper or abstract is expected to present it at the workshop.
Location: the Center of New Technologies ("CeNT"), University of Warsaw in Warsaw, Poland.
More information on the venue of RDP 2015.