Further Reading

• Deterministic Call-By-Need Lambda Calculi
  • Equivalence of Call-by-Name and Call-by-Need
    • Manfred Schmidt-Schauß, David Sabel, and Elena Machkasova.
      Simulation in the call-by-need lambda-calculus with letrec, case, constructors, and seq.
      Frank report 49, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, July 2012.
      [ bib | PDF ]
    • Manfred Schmidt-Schauß, David Sabel, and Elena Machkasova.
      Simulation in the call-by-need lambda-calculus with letrec.
      In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications,
      volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 295-310,
      Dagstuhl, Germany, July 2010. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
      [ bib | PDF | http ]
    • Manfred Schmidt-Schauß, David Sabel, and Elena Machkasova.
      Simulation in the call-by-need lambda-calculus with letrec.
      Frank report 40, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, April 2010.
      [ bib | PDF ]
    • Manfred Schmidt-Schauß.
      Correctness of copy in calculi with letrec.
      In Term Rewriting and Applications (RTA-18), volume 4533 of LNCS, pages 329-343. Springer, June 2007. © Springer Verlag.
      [ bib | slides (RTA 2007) ]
    • Manfred Schmidt-Schauß.
      Correctness of copy in calculi with letrec, case, constructors and por.
      Frank report 29, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, February 2007.
      [ PDF ]
    • Manfred Schmidt-Schauß.
      Correctness of copy in calculi with letrec, case and constructors.
      Frank report 28, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, February 2007.
      [ PDF ]
    • Manfred Schmidt-Schauß.
      Equivalence of call-by-name and call-by-need for lambda-calculi with letrec.
      Frank report 25, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, September 2006.
      [ PDF ]
  • Strictness Analysis Using Abstract Reduction
    • Manfred Schmidt-Schauß, Marko Schütz, and David Sabel.
      Safety of Nöcker's strictness analysis.
      Journal of Functional Programming, 18(04):503-551, 2008.
      The original publication is available here, © Cambridge University Press.
      [ bib | appendix | PDF | http ]
    • Manfred Schmidt-Schauß, Marko Schütz, and David Sabel.
      A complete proof of the safety of Nöcker's strictness analysis.
      Frank report 20, Institut für Informatik. J.W.Goethe-Universität Frankfurt am Main, April 2005.
      [ PDF ]
      
    • Manfred Schmidt-Schauß, David Sabel, and Marko Schütz.
      Deciding inclusion of set constants over infinite non-strict data structures.
      RAIRO-Theoretical Informatics and Applications, 41(2):225-241, July 2007.
      The original publication is available at: www.edpsciences.org/ita, © EDP Sciences 2007.
      [ bib | PDF | http ]
    • Manfred Schmidt-Schauß, David Sabel, and Marko Schütz.
      Deciding subset relationship of co-inductively defined set constants.
      Frank report 23, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, September 2006.
      [ PDF ]
      
  • Contextual Equivalence and Polymorphic Typing
    • David Sabel, Manfred Schmidt-Schauß, and Frederik Harwath.
      Reasoning about contextual equivalence: From untyped to polymorphically typed calculi.
      In Stefan Fischer, Erik Maehle, and Rüdiger Reischuk, editors,
      INFORMATIK 2009, Im Focus das Leben, Beiträge der 39. Jahrestagung der Gesellschaft für Informatik e.V. (GI), 28.9 - 2.10.2009 in Lübeck,
      volume 154 of GI Edition - Lecture Notes in Informatics, pages 369; 2931-45, October 2009.
      (4. Arbeitstagung Programmiersprachen (ATPS)), © Gesellschaft für Informatik e.V.
      [ bib | PDF ]
  • Bisimulation, Similarity
    • Manfred Schmidt-Schauß, David Sabel, and Elena Machkasova.
      Simulation in the call-by-need lambda-calculus with letrec.
      In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications,
      volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 295-310, Dagstuhl, Germany, July 2010. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.
      [ bib | PDF | http ]
    • Manfred Schmidt-Schauß, David Sabel, and Elena Machkasova.
      Simulation in the call-by-need lambda-calculus with letrec.
      Frank report 40, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, April 2010.
      [ bib | PDF ]
• Non-Deterministic Call-by-Need Lambda-Calculi
  • Semantics for Haskell extended with direct-call I/O
    • A detailed overview describing the DIAMOND project and links to further references can be found through the DIAMOND project webpage
  • Mutual Similarity and Finite Simulation
    • Manfred Schmidt-Schauß, Elena Machkasova, and David Sabel.
      Counterexamples to simulation in non-deterministic call-by-need lambda-calculi with letrec.
      Frank report 38, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, August 2009.
      [ bib | PDF ]
    • Matthias Mann and Manfred Schmidt-Schauß.
      Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi.
      Information and Computation, 208(3):276 - 291, 2010.
      [ bib | http ]
    • Manfred Schmidt-Schauß and Elena Machkasova.
      A finite simulation method in a non-deterministic call-by-need lambda-calculus with letrec, constructors and case.
      In Rewriting Techniques and Applications (RTA-18), volume 5117 of LNCS, pages 321-335. Springer-Verlag, July 2008. © Springer Verlag.
      [ bib | http ]
    • Manfred Schmidt-Schauß and Elena Machkasova.
      A finite simulation method in a non-deterministic call-by-need calculus with letrec, constructors and case.
      Frank report 32, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, February 2008.
      [ PDF ]
    • Manfred Schmidt-Schauß and Matthias Mann.
      On equivalences and standardization in a non-deterministic call-by-need lambda calculus.
      Frank report 31, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, September 2007.
      [ bib | PDF | previous version ]
    • Matthias Mann and Manfred Schmidt-Schauß.
      How to prove similarity a precongruence in non-deterministic call-by-need lambda calculi.
      Frank report 22, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, January 2006.
      [ PDF ]
    • Matthias Mann.
      A Non-Deterministic Call-by-Need Lambda Calculus: Proving Similarity a Precongruence by an Extension of Howe's Method to Sharing.
      Dissertation, Johann Wolfgang Goethe-Universität, Frankfurt, 2005.
      [ German Abstract | PDF ]
    • Matthias Mann.
      Congruence of bisimulation in a non-deterministic call-by-need lambda calculus.
      Electronic Notes in Theoretical Computer Science, 128(1):81-101, May 4, 2005.
      [ http | Corrigendum ]
    • Matthias Mann.
      Towards Sharing in Lazy Computation Systems.
      Frank report 18, Institut für Informatik, J.W. Goethe-Universität Frankfurt am Main, December 2004.
      Available on request.
      
  • Semantics and Transformations for Functional Hardware Descriptions
    • Manfred Schmidt-Schauß and David Sabel.
      Program transformation for functional circuit descriptions.
      Frank report 30, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, February 2007.
      [ PDF ]
      We gave a talk on the topic at the Workshop on Hardware design using Functional Languages (HFL 07)
  • Locally Bottom-Avoiding Choice
    • David Sabel.
      Semantik eines verzögert auswertenden Lambdakalküls mit McCarthy's amb für Programmäquivalenz.
      In Dorothea Wagner et. al., editor, Ausgezeichnete Informatikdissertationen 2008,
      volume D-9 of GI-Edition Lecture Notes in Informatics (LNI) - Dissertations, pages 221-230,
      Bonn, Germany, 2009. Köllen Druck+Verlag. © Gesellschaft für Informatik e.V.
      [ bib | PDF ]
    • David Sabel.
      Semantics of a Call-by-Need Lambda Calculus with McCarthy's amb for Program Equivalence.
      Dissertation, J. W. Goethe-Universität Frankfurt, Institut für Informatik. Fachbereich Informatik und Mathematik, November 2008.
      © Published by Verlag Dr. Hut with ISBN 978-3-89963-866-0.
      [ bib | PDF ]
    • David Sabel and Manfred Schmidt-Schauß.
      A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations.
      Mathematical Structures in Computer Science, 18(03):501-553,2008.
      [ bib | http ]
    • David Sabel and Manfred Schmidt-Schauß.
      A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations.
      Frank report 24, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, July 2006.
      [ bib | PDF ]
• Concurrency, Process Calculi, Adequacy of Encodings
  • STM Haskell
    • Manfred Schmidt-Schauß and David Sabel.
      Correctness of an STM Haskell implementation.
      Frank report 50, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, October 2012.
      [ bib | PDF, Prototype in Haskell]
  • Concurrent Haskell
    • David Sabel and Manfred Schmidt-Schauß.
      Conservative concurrency in Haskell.
      In Nachum Dershowitz, editor, Proceedings of the 27th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2012), 25-28 June 2012, Dubrovnik, Croatia, pages 561-570, June 2012. © IEEE.
      [ bib | slides (LICS 2012) | PDF ]
    • David Sabel and Manfred Schmidt-Schauß.
      On conservativity of Concurrent Haskell.
      Frank report 47, Institut für Informatik, Goethe-Universität Frankfurt am Main, April 2012.
      [ bib | PDF | previous version ]
    • David Sabel.
      An abstract machine for Concurrent Haskell with futures.
      Frank report 48, Institut für Informatik, Goethe-Universität Frankfurt am Main, February 2012.
      [ bib | PDF ]
    • David Sabel.
      An abstract machine for Concurrent Haskell with futures.
      In Stefan Jähnichen, Bernhard Rumpe, and Holger Schlingloff, editors, Software Engineering 2012 Workshopband, Fachtagung des GI-Fachbereichs Softwaretechnik, 27. Februar - 2. März 2012 in Berlin, volume 199 of GI Edition - Lecture Notes in Informatics, pages 29-44, February 2012. (5. Arbeitstagung Programmiersprachen (ATPS'12)), © Gesellschaft für Informatik e.V.
      [ bib | slides (ATPS 2012) | PDF ]
    • David Sabel and Manfred Schmidt-Schauß.
      A contextual semantics for concurrent haskell with futures.
      In Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming, PPDP '11, pages 101-112, New York, NY, USA, July 2011. ACM. © ACM, 2011.
      [ bib | http ]
    • David Sabel and Manfred Schmidt-Schauß.
      A contextual semantics for concurrent Haskell with futures.
      Frank report 44, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, March 2011.
      [ bib | PDF ]
  • Concurrency Primitives and Correctness of Implementations/Translations
    • Jan Schwinghammer, David Sabel, Manfred Schmidt-Schauß, and Joachim Niehren.
      Correctly translating concurrency primitives.
      In ML '09: Proceedings of the 2009 ACM SIGPLAN workshop on ML, pages 27-38, New York, NY, USA, August 2009. ACM. © ACM.
      [ bib | http ]
    • Jan Schwinghammer, David Sabel, Joachim Niehren, and Manfred Schmidt-Schauß.
      On correctness of buffer implementations in a concurrent lambda calculus with futures.
      Frank report 37, Institut für Informatik. Fachbereich Informatik und Mathematik. Goethe-Universität Frankfurt am Main, May 2009.
      [ bib | PDF ]
    • Jan Schwinghammer, David Sabel, Joachim Niehren, and Manfred Schmidt-Schauß.
      On proving the equivalence of concurrency primitives.
      Frank report 34, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, October 2008.
      [ bib | PDF ]
    • Manfred Schmidt-Schauß, Joachim Niehren, Jan Schwinghammer, and David Sabel.
      Adequacy of compositional translations for observational semantics.
      In Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, and C.-H. Luke Ong, editors,
      Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008,
      IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, September 7-10, 2008, Milano, Italy,
      volume 273 of IFIP, pages 521-535. Springer, September 2008. © Springer Verlag.
      [ bib ]
    • Manfred Schmidt-Schauß, Joachim Niehren, Jan Schwinghammer, and David Sabel.
      Adequacy of compositional translations for observational semantics.
      Frank report 33, Institut für Informatik. Fachbereich Informatik und Mathematik. J. W. Goethe-Universität Frankfurt am Main, February 2009.
      [ bib | PDF]
• Automatic Correctness Proofs of Program Transformations
  • Publications
    • Conrad Rau, David Sabel, and Manfred Schmidt-Schauß.
      Correctness of program transformations as a termination problem.
      In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Automated Reasoning - Proceedings of the 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012, volume 7364 of Lecture Notes in Computer Science, pages 462-476. Springer Berlin / Heidelberg, June 2012. © Springer Verlag, The original publication is available at www.springerlink.com.
      [ bib | PDF ]
    • Conrad Rau and Manfred Schmidt-Schauß.
      Towards correctness of program transformations through unification and critical pair computation.
      Frank report 41, Institut für Informatik. Fachbereich Informatik und Mathematik. Goethe-Universität Frankfurt am Main, January 2011.
      [ bib | PDF]
    • Conrad Rau and Manfred Schmidt-Schauß.
      Towards correctness of program transformations through unification and critical pair computation.
      In Proceedings of the 24th International Workshop on Unification, Electronic Proceedings in Theoretical Computer Science, December 2010.
      [ bib | PDF ]
  • You may also visit the project home page
• Algorithms on Grammar-Compressed Strings and Trees
  • A Haskell cabal package can be found here.
  • Manfred Schmidt-Schauß, David Sabel, and Altug Anis. Congruence closure of compressed terms in polynomial time. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, Frontiers of Combining Systems, volume 6989 of Lecture Notes in Computer Science, pages 227-242. Springer Berlin / Heidelberg, October 2011. © Springer Verlag, The original publication is available at www.springerlink.com .
    [ bib | PDF | http ]