First International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2014, July 13, 2014, Vienna, Austria
WPTE 2014
July 13, 2014
Vienna, Austria
Open Access Series in Informatics
OASIcs
https://www.dagstuhl.de/dagpub/2190-6807
https://dblp.org/db/series/oasics
2190-6807
Manfred
Schmidt-Schauß
Manfred Schmidt-Schauß
Masahiko
Sakai
Masahiko Sakai
David
Sabel
David Sabel
Yuki
Chiba
Yuki Chiba
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
40
2014
978-3-939897-70-5
https://www.dagstuhl.de/dagpub/978-3-939897-70-5
Frontmatter, Table of Contents, Preface, Workshop Organization
Frontmatter, Table of Contents, Preface, Workshop Organization
Frontmatter
Table of Contents
Preface
Workshop Organization
i-xv
Front Matter
Manfred
Schmidt-Schauß
Manfred Schmidt-Schauß
Masahiko
Sakai
Masahiko Sakai
David
Sabel
David Sabel
Yuki
Chiba
Yuki Chiba
10.4230/OASIcs.WPTE.2014.i
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
HERMIT: An Equational Reasoning Model to Implementation Rewrite System for Haskell (Invited Talk)
HERMIT is a rewrite system for Haskell.
Program Transformation
Equational Reasoning
Optimization
1-1
Invited Talk
Andrew
Gill
Andrew Gill
10.4230/OASIcs.WPTE.2014.1
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems
Transforming conditional term rewrite systems (CTRSs) into unconditional systems (TRSs) is a common approach to analyze properties of CTRSs via the simpler framework of unconditional rewriting. In the past many different transformations have been introduced for this purpose. One class of transformations, so-called unravelings, have been analyzed extensively in the past.
In this paper we provide an overview on another class of transformations that we call structure-preserving transformations. In these transformations the structure of the conditional rule, in particular their left-hand side is preserved in contrast to unravelings. We provide an overview of transformations of this type and define a new transformation that improves previous approaches.
conditional term rewriting
unraveling
condition elimination
3-14
Regular Paper
Karl
Gmeiner
Karl Gmeiner
Naoki
Nishida
Naoki Nishida
10.4230/OASIcs.WPTE.2014.3
Sergio Antoy, Bernd Brassel, and Michael Hanus. Conditional narrowing without conditions. In Proc. 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 27-29 August 2003, Uppsala, Sweden, pages 20-31. ACM Press, 2003.
Jan A. Bergstra and Jan Willem Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences, 32(3):323-362, 1986.
Elio Giovanetti and Corrado Moiso. Notes on the elimination of conditions. In Stéphane Kaplan and Jean-Pierre Jouannaud, editors, Proc. 1st Int. Workshop on Conditional Rewriting Systems (CTRS'87), Orsay, France, 1987, volume 308 of Lecture Notes in Computer Science, pages 91-97, Orsay, France, 1988. Springer. ISBN 3-540-19242-5.
Karl Gmeiner and Bernhard Gramlich. Transformations of conditional rewrite systems revisited. In Andrea Corradini and Ugo Montanari, editors, Recent Trends in Algebraic Development Techniques (WADT 2008) - Selected Papers, volume 5486 of Lecture Notes in Computer Science, pages 166-186. Springer, 2009.
Karl Gmeiner, Bernhard Gramlich, and Felix Schernhammer. On (un)soundness of unravelings. In Christopher Lynch, editor, Proc. 21st International Conference on Rewriting Techniques and Applications (RTA 2010), July 11-13, 2010, Edinburgh, Scotland, UK, LIPIcs (Leibniz International Proceedings in Informatics), July 2010.
Karl Gmeiner, Bernhard Gramlich, and Felix Schernhammer. On soundness conditions for unraveling deterministic conditional rewrite systems. In Ashish Tiwari, editor, Proc. 23rd International Conference on Rewriting Techniques and Applications (RTA 2012), May 30 to June 2, 2012, Nagoya, Japan, LIPIcs (Leibniz International Proceedings in Informatics), May/June 2012.
Karl Gmeiner, Naoki Nishida, and Bernhard Gramlich. Proving confluence of conditional term rewriting systems via unravelings. In Nao Hirokawa and Vincent van Oostrom, editors, Proceedings of the 2nd International Workshop on Confluence, pages 35-39, 2013.
Claus Hintermeier. How to transform canonical decreasing ctrss into equivalent canonical trss. In Conditional and Typed Rewriting Systems, 4th International Workshop, CTRS-94, Jerusalem, Israel, July 13-15, 1994, Proceedings, volume 968 of Lecture Notes in Computer Science, pages 186-205, 1995.
Massimo Marchiori. Unravelings and ultra-properties. In Michael Hanus and Mario Mario Rodríguez-Artalejo, editors, Proc. 5th Int. Conf. on Algebraic and Logic Programming, Aachen, volume 1139 of Lecture Notes in Computer Science, pages 107-121. Springer, September 1996.
Massimo Marchiori. On deterministic conditional rewriting. Technical Report MIT LCS CSG Memo n.405, MIT, Cambridge, MA, USA, October 1997.
Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe. Partial inversion of constructor term rewriting systems. In Jürgen Giesl, editor, Proc. 16th International Conference on Rewriting Techniques and Applications (RTA'05), Nara, Japan, April 19-21, 2005, volume 3467 of Lecture Notes in Computer Science, pages 264-278. Springer, April 2005.
Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe. Soundness of unravelings for deterministic conditional term rewriting systems via ultra-properties related to linearity. In Manfred Schmidt-Schauss, editor, Proc. 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), May 30 to June 1, 2011, Novi Sad, Serbia, LIPIcs (Leibniz International Proceedings in Informatics), 2011. pages 267-282.
Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002.
Grigore Rosu. From conditional to unconditional rewriting. In José Luiz Fiadeiro, Peter D. Mosses, and Fernando Orejas, editors, WADT, volume 3423 of Lecture Notes in Computer Science, pages 218-233. Springer, 2004.
Traian-Florin Şerbănuţă and Grigore Roşu. Computationally equivalent elimination of conditions. In Frank Pfenning, editor, Proc. 17th International Conference on Rewriting Techniques and Applications, Seattle, WA, USA, August 12-14, 2006, volume 4098 of Lecture Notes in Computer Science, pages 19-34. Springer, 2006.
Patrick Viry. Elimination of conditions. J. Symb. Comput., 28(3):381-401, 1999.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Verifying Optimizations for Concurrent Programs
While program correctness for compiled languages depends fundamentally on compiler correctness, compiler optimizations are not usually formally verified due to the effort involved, particularly in the presence of concurrency. In this paper, we present a framework for stating and reasoning about compiler optimizations and transformations on programs in the presence of relaxed memory models. The core of the framework is the PTRANS specification language, in which program transformations are expressed as rewrites on control flow graphs with temporal logic side conditions. We demonstrate our technique by verifying the correctness of a redundant store elimination optimization in a simple LLVM-like intermediate language, relying on a theorem that allows us to lift single-thread simulation relations to simulations on multithreaded programs.
optimizing compilers
interactive theorem proving
program transformations
temporal logic
relaxed memory models
15-26
Regular Paper
William
Mansky
William Mansky
Elsa L.
Gunter
Elsa L. Gunter
10.4230/OASIcs.WPTE.2014.15
Sebastian Burckhardt, Madanlal Musuvathi, and Vasu Singh. Verifying local transformations on relaxed memory models. In Proceedings of the 19th Joint European Conference on Theory and Practice of Software, International Conference on Compiler Construction, CC'10/ETAPS'10, pages 104-123, Berlin, Heidelberg, 2010. Springer-Verlag.
Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In Jaco de Bakker and Jan van Leeuwen, editors, Automata, Languages and Programming, volume 85 of Lecture Notes in Computer Science, pages 299-309. Springer Berlin / Heidelberg, 1980. URL: http://dx.doi.org/10.1007/3-540-10003-2_79.
http://dx.doi.org/10.1007/3-540-10003-2_79
C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1985.
Sara Kalvala, Richard Warburton, and David Lacey. Program transformations using temporal logic side conditions. ACM Trans. Program. Lang. Syst., 31(4):1-48, 2009.
Jens Krinke. Context-sensitive slicing of concurrent programs. SIGSOFT Softw. Eng. Notes, 28(5):178-187, September 2003.
Sorin Lerner, Todd Millstein, and Craig Chambers. Automatically proving the correctness of compiler optimizations. SIGPLAN Not., 38:220-231, May 2003.
Xavier Leroy. A formally verified compiler back-end. J. Autom. Reason., 43(4):363-446, December 2009.
Hongjin Liang, Xinyu Feng, and Ming Fu. A rely-guarantee-based simulation for verifying concurrent program transformations. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL'12, pages 455-468, New York, NY, USA, 2012. ACM.
LLVM Language Reference Manual. http://llvm.org/docs/LangRef.html, April 2014.
William Mansky, Dennis Griffith, and Elsa L. Gunter. Specifying and executing optimizations for parallel programs. Accepted for publication by GRAPHITE'14.
William Mansky and Elsa Gunter. A framework for formal verification of compiler optimizations. In Proceedings of the First international conference on Interactive Theorem Proving, ITP'10, pages 371-386, Berlin, Heidelberg, 2010. Springer-Verlag.
Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361-386. Academic Press, 1990.
Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In TACAS'98: Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pages 151-166, London, UK, 1998. Springer-Verlag.
Pradeep S. Sindhu, Jean-Marc Frailong, and Michel Cekleov. Formal specification of memory models. In Michel Dubois and Shreekant Thakkar, editors, Scalable Shared Memory Multiprocessors, pages 25-41. Springer US, 1992.
Jaroslav Ševčík. Safe optimisations for shared-memory concurrent programs. SIGPLAN Not., 46(6):306-316, June 2011.
Jaroslav Ševčik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. Relaxed-memory concurrency and verified compilation. SIGPLAN Not., 46(1):43-54, January 2011.
Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. Finding and understanding bugs in C compilers. SIGPLAN Not., 46(6):283-294, June 2011.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Inverse Unfold Problem and Its Heuristic Solving
Unfold/fold transformations have been widely studied in various programming paradigms and are used in program transformations, theorem proving, and so on. This paper, by using an example, show that
restoring an one-step unfolding is not easy, i.e., a challenging task, since some rules used by unfolding may be lost. We formalize this problem by regarding one-step program transformation as a relation. Next we discuss some issues on a specific framework, called pure-constructor systems, which constitute a subclass of conditional term rewriting systems. We show that the inverse of T preserves rewrite relations if T preserves rewrite relations and the signature. We propose a heuristic procedure to solve the problem, and show its successful examples. We improve the procedure, and show examples for which the improvement takes effect.
program transformation
unfolding
conditional term rewriting system
27-38
Regular Paper
Masanori
Nagashima
Masanori Nagashima
Tomofumi
Kato
Tomofumi Kato
Masahiko
Sakai
Masahiko Sakai
Naoki
Nishida
Naoki Nishida
10.4230/OASIcs.WPTE.2014.27
Jesús Manuel Almendros-Jiménez and Germán Vidal. Automatic partial inversion of inductively sequential functions. In Zoltán Horváth, Viktória Zsók, and Andrew Butterfield, editors, Proc. of 18th International Symposium on Implementation and Application of Functional Languages, volume 4449 of Lecture Notes in Computer Science, pages 253-270, 2007.
Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
David Basin and Toby Walsh. Difference matching. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of Lecture Notes in Computer Science, pages 295-309. Springer, 1992.
N. Bensaou and Irène Guessarian. Transforming constraint logic programs. Theoretical Computer Science, 206(1-2):81-125, 1998.
Jan A. Bergstra and Jan Willem Klop. Conditional rewrite rules: Confluence and termination. Journal of Computer and System Sciences, 32(3):323-362, 1986.
Rod M. Burstall and John Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44-67, 1977.
Sandro Etalle and Maurizio Gabbrielli. Transformations of CLP modules. Theoretical Computer Science, 166(1-2):101-146, 1996.
Fabio Fioravanti, Alberto Pettorossi, and Maurizio Proietti. Transformation rules for locally stratified constraint logic programs. In Maurice Bruynooghe and Kung-Kiu Lau, editors, Program Development in Computational Logic, volume 3049 of Lecture Notes in Computer Science, pages 77-89. Springer, 2004.
Harald Ganzinger. Order-sorted completion: The many-sorted way. Theoretical Computer Science, 89(1):3-32, 1991.
Robert Glück and Masahiko Kawabe. A method for automatic program inversion based on LR(0) parsing. Fundamenta Informmaticae, 66(4):367-395, 2005.
Tadashi Kanamori and Kenji Horiuchi. Construction of logic programs based on generalized unfold/fold rules. In Jean-Louis Lassez, editor, Proceedings of the 4th International Conference on Logic Programming, pages 744-768, 1987.
Michael J. Maher. A transformation system for deductive database modules with perfect model semantics. Theoretical Computer Science, 110(2):377-403, 1993.
Aart Middeldorp and Erik Hamoen. Completeness results for basic narrowing. Applicable Algebra in Engineering, Communication and Computing, 5:213-253, 1994.
Masanori Nagashima, Masahiko Sakai, and Toshiki Sakabe. Determinization of conditional term rewriting systems. Theoretical Computer Science, 464:72-89, 2012.
Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe. Partial inversion of constructor term rewriting systems. In Jürgen Giesl, editor, Proc. of the 16th Int'l Conf. on Rewriting Techniques and Applications, volume 3467 of LNCS, pages 264-278. Springer, 2005.
Naoki Nishida and Germán Vidal. Program inversion for tail recursive functions. In Manfred Schmidt-Schauß, editor, Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, volume 10 of LIPIcs, pages 283-298. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011.
Naoki Nishida and Germán Vidal. Computing more specific versions of conditional rewriting systems. In Elvira Albert, editor, Revised Selected Papers of the 22nd International Symposium on Logic-Based, volume 7844 of Lecture Notes in Computer Science, pages 137-154, 2013.
Minami Niwa, Naoki Nishida, and Masahiko Sakai. Extending matching operation in grammar program for program inversion. In Elvira Albert, editor, Informal Proceedings of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2012), pages 130-139, 2012.
Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer-Verlag, 2002.
Alberto Pettorossi, Maurizio Proietti, and Valerio Senni. Constraint-based correctness proofs for logic program transformations. Formal Aspects of Computing, 24(4-6):569-594, 2012.
Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, and I. V. Ramakrishnan. Beyond Tamaki-Sato style unfold/fold transformations for normal logic programs. International Journal of Foundations of Computer Science, 13(3):387-403, 2002.
Abhik Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, and I. V. Ramakrishnan. An unfold/fold transformation framework for definite logic programs. ACM Transactions on Programming Languages and Systems, 26(3):464-509, 2004.
David Sands. Total correctness by local improvement in the transformation of functional programs. ACM Trans. on Programming Languages and Systems, 18(2):175-234, 1996.
Taisuke Sato. Equivalence-preserving first-order unfold/fold transformation systems. Theoretical Computer Science, 105(1):57-84, 1992.
Hirohisa Seki. Unfold/fold transformation of general logic programs for the well-founded semantics. Journal of Logic Programming, 16(1):5-23, 1993.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings
In this paper, we show that the SR transformation, a computationally equivalent transformation proposed by Serbanuta and Rosu, is sound for weakly left-linear normal conditional term rewriting systems (CTRS). Here, soundness for a CTRS means that reduction of the transformed unconditional term rewriting system (TRS) creates no undesired reduction for the CTRS. We first show that every reduction sequence of the transformed TRS starting with a term corresponding to the one considered on the CTRS is simulated by the reduction of the TRS obtained by the simultaneous unraveling. Then, we use the fact that the unraveling is sound for weakly left-linear normal CTRSs.
conditional term rewriting
unraveling
condition elimination
39-50
Regular Paper
Naoki
Nishida
Naoki Nishida
Makishi
Yanagisawa
Makishi Yanagisawa
Karl
Gmeiner
Karl Gmeiner
10.4230/OASIcs.WPTE.2014.39
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Structural Rewriting in the pi-Calculus
We consider reduction in the synchronous pi-calculus with replication, without sums. Usual definitions of reduction in the pi-calculus use a closure w.r.t. structural congruence
of processes. In this paper we operationalize structural congruence by providing a reduction relation for pi-processes which also performs necessary structural conversions explicitly by
rewrite rules. As we show, a subset of structural congruence axioms is sufficient. We show that our rewrite strategy is equivalent to the usual strategy including structural congruence w.r.t.the observation of barbs and thus w.r.t. may- and should-testing equivalence in the pi-calculus.
Process calculi
Rewriting
Semantics
51-62
Regular Paper
David
Sabel
David Sabel
10.4230/OASIcs.WPTE.2014.51
M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. In CCS'97, pages 36-47. ACM, 1997.
J. Engelfriet and T. Gelsema. A new natural structural congruence in the pi-calculus with replication. Acta Inf., 40(6-7):385-430, 2004.
J. Engelfriet and T. Gelsema. An exercise in structural congruence. Inf. Process. Lett., 101(1):1-5, 2007.
C. Fournet and G. Gonthier. A hierarchy of equivalences for asynchronous calculi. J. Log. Algebr. Program., 63(1):131-173, 2005.
J. Giesl, P. Schneider-Kamp, and R. Thiemann. Automatic termination proofs in the dependency pair framework. In IJCAR'06, volume 4130 of LNCS, pages 281-286. Springer, 2006.
V. Khomenko and R. Meyer. Checking pi-calculus structural congruence is graph isomorphism complete. In ACSD'09, pages 70-79. IEEE, 2009.
C. Laneve. On testing equivalence: May and must testing in the join-calculus. Technical Report UBLCS 96-04, University of Bologna, 1996.
R. Milner. Communicating and Mobile Systems: the π-calculus. CUP, 1999.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, i &ii. Inform. and Comput., 100(1):1-77, 1992.
J. H. Morris. Lambda-Calculus Models of Programming Languages. PhD thesis, MIT, 1968.
V. Natarajan and R. Cleaveland. Divergence and fair testing. In ICALP'95, volume 944 of LNCS, pages 648-659. Springer, 1995.
J. Niehren, D. Sabel, M. Schmidt-Schauß, and J. Schwinghammer. Observational semantics for a concurrent lambda calculus with reference cells and futures. Electron. Notes Theor. Comput. Sci., 173:313-337, 2007.
G. D. Plotkin. Call-by-name, call-by-value, and the lambda-calculus. Theoret. Comput. Sci., 1:125-159, 1975.
C. Priami. Stochastic pi-calculus. Comput. J., 38(7):578-589, 1995.
C. Rau, D. Sabel, and M. Schmidt-Schauß. Correctness of program transformations as a termination problem. In IJCAR'12, volume 7364 of LNCS, pages 462-476. Springer, 2012.
A. Rensink and W. Vogler. Fair testing. Inform. and Comput., 205(2):125-198, 2007.
D. Sabel and M. Schmidt-Schauß. A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations. Math. Structures Comput. Sci., 18(03):501-553, 2008.
D. Sabel and M. Schmidt-Schauß. A contextual semantics for Concurrent Haskell with futures. In PPDP'11, pages 101-112. ACM, 2011.
D. Sabel and M. Schmidt-Schauß. Conservative concurrency in Haskell. In LICS'12, pages 561-570. IEEE, 2012.
D. Sabel and M. Schmidt-Schauß. Contextual equivalence for the pi-calculus that can stop. Frank report 53, J. W. Goethe-Universität Frankfurt am Main, 2014. URL: http://www.ki.cs.uni-frankfurt.de/papers/frank/pi-stop-frank.pdf.
http://www.ki.cs.uni-frankfurt.de/papers/frank/pi-stop-frank.pdf
D. Sangiorgi and D. Walker. The π-calculus: a theory of mobile processes. CUP, 2001.
M. Schmidt-Schauß, C. Rau, and D. Sabel. Algorithms for Extended Alpha-Equivalence and Complexity. In RTA'13, volume 21 of LIPIcs, pages 255-270. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2013.
M. Schmidt-Schauß and D. Sabel. Correctness of an STM Haskell implementation. In ICFP'13, pages 161-172. ACM, 2013.
R. Thiemann and C. Sternagel. Certification of termination proofs using CeTA. In TPHOLs'09, volume 5674 of LNCS, pages 452-468. Springer, 2009.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary Report)
This paper presents a call-by-need polymorphically typed lambda-calculus with letrec, case, constructors and seq. The typing of the calculus is modelled in a system-F style. Contextual equivalence is used as semantics of expressions. We also define a call-by-name variant without letrec. We adapt several tools and criteria for recognizing correct program transformations to polymorphic typing, in particular an inductive applicative simulation.
functional programming
polymorphic typing
contextual equivalence
semantics
63-74
Preliminary Report
Manfred
Schmidt-Schauß
Manfred Schmidt-Schauß
David
Sabel
David Sabel
10.4230/OASIcs.WPTE.2014.63
S. Abramsky. The lazy lambda calculus. In D. A. Turner, editor, Research Topics in Functional Programming, pages 65-116. Addison-Wesley, 1990.
Z. M. Ariola and J. W. Klop. Lambda calculus with explicit recursion. Inform. and Comput., 139(2):154-233, 1997.
J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. CUP, 1994.
Haskell-community. The Haskell Programming Language, 2014. http://www.haskell.org.
D. Howe. Equality in lazy computation systems. In LICS'89, pages 198-203, 1989.
D. Howe. Proving congruence of bisimulation in functional programming languages. Inform. and Comput., 124(2):103-112, 1996.
J. Launchbury. A natural semantics for lazy evaluation. In POPL'93, pages 144-154. ACM, 1993.
A. K. D. Moran, D. Sands, and M. Carlsson. Erratic fudgets: A semantic theory for an embedded coordination language. Sci. Comput. Program., 46(1-2):99-135, 2003.
S. Peyton Jones. Haskell 98 language and libraries: the Revised Report. CUP, 2003.
B. C. Pierce. Types and Programming Languages. The MIT Press, 2002.
A. M. Pitts. Howe’s method for higher-order languages. In Advanced Topics in Bisimulation and Coinduction, volume 52 of Cambridge Tracts in Theoretical Computer Science, chapter 5, pages 197-232. CUP, November 2011. (chapter 5).
D. Sabel and M. Schmidt-Schauß. A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations. Math. Structures Comput. Sci., 18(03):501-553, 2008.
D. Sabel and M. Schmidt-Schauß. A contextual semantics for Concurrent Haskell with futures. In PPDP'11, pages 101-112, New York, NY, USA, July 2011. ACM.
D. Sabel and M. Schmidt-Schauß. Conservative concurrency in Haskell. In LICS'12, pages 561-570. IEEE, 2012.
D. Sabel, M. Schmidt-Schauß, and F. Harwath. Reasoning about contextual equivalence: From untyped to polymorphically typed calculi. In INFORMATIK 2009 (ATPS'09), volume 154 of LNI, pages 369; 2931-45, 2009.
M. Schmidt-Schauß. Correctness of copy in calculi with letrec. In RTA'08, volume 4533 of LNCS, pages 329-343. Springer, 2007.
M. Schmidt-Schauß, E. Machkasova, and D. Sabel. Extending Abramsky’s lazy lambda calculus: (non)-conservativity of embeddings. In RTA'13, volume 21 of LIPIcs, pages 239-254, Dagstuhl, Germany, 2013. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
M. Schmidt-Schauß and D. Sabel. On generic context lemmas for higher-order calculi with sharing. Theoret. Comput. Sci., 411(11-13):1521 - 1541, 2010.
M. Schmidt-Schauß, D. Sabel, and E. Machkasova. Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec. Inf. Process. Lett., 111(14):711-716, 2011.
M. Schmidt-Schauß, D. Sabel, and E. Machkasova. Simulation in the call-by-need lambda-calculus with letrec, case, constructors, and seq. Frank report 49, Goethe-Universität Frankfurt, 2012.
M. Schmidt-Schauß, M. Schütz, and D. Sabel. Safety of Nöcker’s strictness analysis. J. Funct. Programming, 18(04):503-551, 2008.
J. Voigtländer and P. Johann. Selective strictness and parametricity in structural operational semantics, inequationally. Theor. Comput. Sci, 388(1-3):290-318, 2007.
D. Vytiniotis and S. Peyton Jones. Evidence Normalization in System FC (Invited Talk). In RTA'13, volume 21 of LIPIcs, pages 20-38, Dagstuhl, Germany, 2013. Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode