2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015), WPTE 2015, July 2, 2015, Warsaw, Poland
WPTE 2015
July 2, 2015
Warsaw, Poland
Open Access Series in Informatics
OASIcs
https://www.dagstuhl.de/dagpub/2190-6807
https://dblp.org/db/series/oasics
2190-6807
Yuki
Chiba
Yuki Chiba
Santiago
Escobar
Santiago Escobar
Naoki
Nishida
Naoki Nishida
David
Sabel
David Sabel
Manfred
Schmidt-Schauß
Manfred Schmidt-Schauß
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
46
2015
978-3-939897-94-1
https://www.dagstuhl.de/dagpub/978-3-939897-94-1
Frontmatter, Table of Contents, Preface, Workshop Organization
Frontmatter, Table of Contents, Preface, Workshop Organization
Frontmatter
Table of Contents
Preface
Workshop Organization
i-xvi
Front Matter
Yuki
Chiba
Yuki Chiba
Santiago
Escobar
Santiago Escobar
Naoki
Nishida
Naoki Nishida
David
Sabel
David Sabel
Manfred
Schmidt-Schauß
Manfred Schmidt-Schauß
10.4230/OASIcs.WPTE.2015.i
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Mechanizing Meta-Theory in Beluga (Invited Talk)
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. The Beluga system together with examples is available from http://complogic.cs.mcgill.ca/beluga.
Type systems
Dependent Types
Logical Frameworks
1-1
Invited Talk
Brigitte
Pientka
Brigitte Pientka
10.4230/OASIcs.WPTE.2015.1
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Head reduction and normalization in a call-by-value lambda-calculus
Recently, a standardization theorem has been proven for a variant of Plotkin's call-by-value lambda-calculus extended by means of two commutation rules (sigma-reductions): this result was based on a partitioning between head and internal reductions. We study the head normalization for this call-by-value calculus with sigma-reductions and we relate it to the weak evaluation of original Plotkin's call-by-value lambda-calculus. We give also a (non-deterministic) normalization strategy for the call-by-value lambda-calculus with sigma-reductions.
sequentialization
lambda-calculus
sigma-reduction
call-by-value
head reduction
internal reduction
(strong) normalization
evaluation
confluence
3-17
Regular Paper
Giulio
Guerrieri
Giulio Guerrieri
10.4230/OASIcs.WPTE.2015.3
Beniamino Accattoli. Proof nets and the call-by-value lambda-calculus. In Delia Kesner and Petrucio Viana, editors, Proceedings Seventh Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2012, volume 113 of EPTCS, pages 11-26, 2012.
Beniamino Accattoli and Luca Paolini. Call-by-Value Solvability, Revisited. In Tom Schrijvers and Peter Thiemann, editors, Functional and Logic Programming, volume 7294 of Lecture Notes in Computer Science, pages 4-16. Springer-Verlag, 2012.
Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in logic and the foundation of mathematics. North Holland, 1984.
Alberto Carraro and Giulio Guerrieri. A Semantical and Operational Account of Call-by-Value Solvability. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures, volume 8412 of Lecture Notes in Computer Science, pages 103-118. Springer-Verlag, 2014.
Karl Crary. A Simple Proof of Call-by-Value Standardization. Technical Report CMU-CS-09-137, Carnegie Mellon University, 2009.
Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-102, 1987.
Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. Standardization of a call-by-value lambda-calculus. In To appear in the Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15), 2015. Available at URL: http://www.pps.univ-paris-diderot.fr/~giuliog/standard.pdf.
http://www.pps.univ-paris-diderot.fr/~giuliog/standard.pdf
Hugo Herbelin and Stéphane Zimmermann. An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, volume 5608 of Lecture Notes in Computer Science, pages 142-156. Springer-Verlag, 2009.
Peter J. Landin. A correspondence between ALGOL 60 and Church's lambda notation. Communications of the ACM, 8:89-101; 158-165, 1965.
John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Theoretical Computer Science, 228(1-2):175-210, 1999.
Eugenio Moggi. Computational Lambda-Calculus and Monads. In Logic in Computer Science, pages 14-23. IEEE Computer Society, 1989.
Luca Paolini. Call-by-Value Separability and Computability. In Antonio Restivo, Simona Ronchi Della Rocca, and Luca Roversi, editors, Italian Conference in Theoretical Computer Science, volume 2202 of Lecture Notes in Computer Science, pages 74-89. Springer-Verlag, 2002.
Luca Paolini and Simona Ronchi Della Rocca. Call-by-value Solvability. Theoretical Informatics and Applications, 33(6):507-534, 1999. RAIRO Series, EDP-Sciences.
Luca Paolini and Simona Ronchi Della Rocca. The Parametric λ-Calculus: a Metamodel for Computation. Texts in Theoretical Computer Science: An EATCS Series. Springer-Verlag, 2004.
Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science, 1(2):125-159, 1975.
Laurent Regnier. Lambda calcul et réseaux. PhD thesis, Université Paris 7, 1992.
Laurent Regnier. Une équivalence sur les lambda-termes. Theoretical Computer Science, 126(2):281-292, April 1994.
Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and symbolic computation, 6(3-4):289-360, 1993.
Masako Takahashi. Parallel reductions in lambda-calculus. Information and Computation, 118(1):120-127, 1995.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Towards Modelling Actor-Based Concurrency in Term Rewriting
In this work, we introduce a scheme for modelling actor systems within sequential term rewriting. In our proposal, a TRS consists of the union of three components: the functional part (which is specific of a system), a set of rules for reducing concurrent actions, and a set of rules for defining a particular scheduling policy. A key ingredient of our approach is that concurrent systems are modelled by terms in which concurrent actions can never occur inside user-defined function calls. This assumption greatly simplifies the definition of the semantics for concurrent actions, since no term traversal will be needed. We prove that these systems are well defined in the sense that concurrent actions can always be reduced.
Our approach can be used as a basis for modelling actor-based concurrent programs, which can then be analyzed using existing techniques for term rewrite systems.
concurrency
actor model
rewriting
19-29
Regular Paper
Adrián
Palacios
Adrián Palacios
Germán
Vidal
Germán Vidal
10.4230/OASIcs.WPTE.2015.19
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Observing Success in the Pi-Calculus
A contextual semantics - defined in terms of successful termination and may- and should-convergence - is analyzed in the synchronous pi-calculus with replication and a constant Stop to denote success.
The contextual ordering is analyzed, some nontrivial process equivalences are proved, and proof tools for showing contextual equivalences are provided. Among them are a context lemma and new notions of sound applicative similarities for may- and should-convergence. A further result is that contextual equivalence in the pi-calculus with Stop conservatively extends barbed testing equivalence in the (Stop-free) pi-calculus and thus results on contextual equivalence can be transferred to the (Stop-free) pi-calculus with barbed testing equivalence.
Concurrency
Process calculi
Pi-calculus
Rewriting
Semantics
31-46
Regular Paper
David
Sabel
David Sabel
Manfred
Schmidt-Schauß
Manfred Schmidt-Schauß
10.4230/OASIcs.WPTE.2015.31
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Formalizing Bialgebraic Semantics in PVS 6.0
Both operational and denotational semantics are prominent approaches for reasoning about properties of programs and programming languages. In the categorical framework developed by Turi and Plotkin both styles of semantics are unified using a single, syntax independent format, known as GSOS, in which the operational rules of a language are specified. From this format, the operational and denotational semantics are derived. The approach of Turi and Plotkin is based on the categorical notion of bialgebras. In this paper we specify this work in the theorem prover PVS, and prove the adequacy theorem of this formalization. One of our goals is to investigate whether PVS is adequately suited for formalizing metatheory. Indeed, our experiments show that the original categorical framework can be formalized conveniently. Additionally, we present a GSOS specification for the simple imperative programming language While, and execute the derived semantics for a small example program.
operational semantics
denotational semantics
bialgebras
distributive laws
adequacy
theorem proving
PVS
WHILE
47-61
Regular Paper
Sjaak
Smetsers
Sjaak Smetsers
Ken
Madlener
Ken Madlener
Marko
van Eekelen
Marko van Eekelen
10.4230/OASIcs.WPTE.2015.47
Michael Barr and Charles Wells. Category theory for computing science, volume 49. Prentice Hall New York, 1990.
Falk Bartels. On generalised coinduction and probabilistic specification formats. PhD thesis, CWI, Amsterdam, April 2004.
Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. J. ACM, 42(1):232-268, January 1995.
Marcello M Bonsangue, Helle Hvid Hansen, Alexander Kurz, and Jurriaan Rot. Presenting distributive laws. In Algebra and Coalgebra in Computer Science, LNCS, pages 95-109. Springer, 2013.
Ben Delaware, Bruno C.d.S. Oliveira, and Tom Schrijvers. Meta-theory à la carte. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '13, New York, NY, USA, 2013. ACM.
Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS '99, pages 193-202, Washington, DC, USA, 1999. IEEE Computer Society.
Marcelo Fiore and Sam Staton. A congruence rule format for name-passing process calculi from mathematical structural operational semantics. In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, LICS '06, pages 49-58, Washington, DC, USA, 2006. IEEE Computer Society.
Ulrich Hensel and Bart Jacobs. Coalgebraic theories of sequences in pvs. J. Log. Comput., 9(4):463-500, 1999.
Ralf Hinze and Daniel W.H. James. Proving the unique fixed-point principle correct: an adventure with category theory. SIGPLAN Not., 46(9):359-371, September 2011.
Bart Jacobs and Jan Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:62-222, 1997.
Mauro Jaskelioff, Neil Ghani, and Graham Hutton. Modularity and implementation of mathematical operational semantics. Electron. Notes Theor. Comput. Sci., 229(5):75-95, March 2011.
Bartek Klin. Bialgebras for structural operational semantics: An introduction. Theoretical Computer Science, 412(38):5043-5069, 2011. CMCS Tenth Anniversary Meeting.
Sheng Liang, Paul Hudak, and Mark Jones. Monad transformers and modular interpreters. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '95, pages 333-343, New York, NY, USA, 1995. ACM.
Ken Madlener and Sjaak Smetsers. GSOS formalized in Coq. In The 7th International Symposium on Theoretical Aspects of Software Engineering (TASE2013), pages 199-206, 2013. Birmingham, UK, 2013. IEEE.
Ken Madlener, Sjaak Smetsers, and Marko C. J. D. van Eekelen. Formal component-based semantics. In Michel A. Reniers and Pawel Sobocinski, editors, SOS, volume 62 of EPTCS, pages 17-29, 2011.
Erik Meijer, Maarten M. Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture, pages 124-144, London, UK, UK, 1991. Springer-Verlag.
Hanne Riis Nielson and Flemming Nielson. Semantics with applications: a formal introduction. John Wiley &Sons, Inc., New York, NY, USA, 1992.
Daniele Turi and Gordon Plotkin. Towards a mathematical operational semantics. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, LICS '97, pages 280-291, Washington, DC, USA, 1997. IEEE Computer Society.
Philip Wadler. Theorems for free! In Functional Programming Languages And Computer Architecture, pages 347-359. ACM Press, 1989.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode