Redirecting to  http://dwolfram.googlepages.com/cttcites. Please update links.

Some Citations of
The Clausal Theory of Types

front cover of The Clausal Theory of Types


D.A. Wolfram
Cambridge Tracts in Theoretical Computer Science
Volume 21. viii+124 pages. ISBN 0 521 39538 0.
© Cambridge University Press 1993.


BiBTeX Entry

@book{Tracts21,
      AUTHOR = "D.A.\ Wolfram",
      TITLE = "The {C}lausal {T}heory of {T}ypes",
      PUBLISHER = "Cambridge University Press",
      YEAR = "1993",
      VOLUME = "21",
      SERIES = "Cambridge Tracts in Theoretical Computer Science"}
 

Chapter 2 Simply Typed lambda-Calculus

  1. Manuel M. T. Chakravarty, Yike Guo, Martin Köhler and Hendrik Lock.
    Goffin: Higher-order functions meet concurrent constraints, Science of Computer Programming (1998) 30(1-2):157-199.
  2. Robert W. Hasker.
    The Replay of Program Derivations, PhD Dissertation, University of Illinois at Urbana-Champaign, 1995, 225 pp.
  3. Jan Malolepszy, Malgorzata Moczurad, and Marek Zaionc.
    Schwichtenberg-style lambda definability is undecidable, Typed Lambda Calculus and Applications, Lecture Notes in Computer Science 1210, (Springer, Berlin, 1997) 267-283.
  4. Malgorzata Moczurad, Jerzy Tyszkiewicz and Marek Zaionc.
    Statistical properties of simple types, School of Computer Science and Engineering, The University of New South Wales, Australia, Technical Report UNSW-CSE-TR-9808, 29 pp., 1998. Submitted to Mathematical Structures in Computer Science.
  5. Manfred Schmidt-Schauß and Klaus U. Schultz
    Decidability of Bounded Higher-Order Unification, Computer Science Logic, 16th International Workshop, CSL 2002, Lecture Notes in Computer Science 2471, (Springer, Berlin, 2002) 522-536.
  6. Marek Zaionc.
    Fixpoint technique for counting terms in typed lambda-calculus, Technical Report 95-20, Department of Computer Science, State University of New York at Buffalo, 1995.
  7. Marek Zaionc.
    Lambda definability is decidable for second order types and for regular third order types, Technical Report 95-24, Department of Computer Science, State University of New York at Buffalo, 1995.

Section 2.4 Normal Forms

  1. Ken Mano and Mizuhito Ogawa.
    Unique normal form property of higher-order rewriting systems, Algebraic and Logic Programming, Lecture Notes in Computer Science 1139, (Springer, Berlin, 1996) 269-283.

Chapter 3 Higher-Order Logic

  1. Peter B. Andrews.
    Classical type theory, in: Alan Robinson and Andrei Voronkov, Eds., Handbook of Automated Reasoning, (Elsevier Science, Amsterdam, 2001) pp. 965-1007.
  2. Peter B. Andrews.
    An Introduction to Mathematical Logic and Type Theory: To Truth through Proof, Vol. 27 Applied Logic Series, Kluwer Academic, Second Edition, 2002.
  3. John Lloyd.
    Declarative Programming in Escher, Technical Report CSTR-95-013, June 1995 (Revised August 1995), Department of Computer Science, University of Bristol.
  4. John Lloyd.
    Programming in an Integrated Functional and Logic Language, The Journal of Functional and Logic Programming, 1999, 3 (1999) 1-49.
  5. John Lloyd.
    Logic and Learning: Learning Comprehensible Theories from Structured Data, (Springer, Berlin, 2003), 250 pp.

Section 3.3 General Models

  1. Manuel M. T. Chakravarty, Yike Guo, Martin Köhler and Hendrik Lock.
    Goffin: Higher-order functions meet concurrent constraints, Science of Computer Programming (1998) 30(1-2):157-199.

Section 4.1 Higher-Order Equational Unification

  1. Zhenyu Qian and Kang Wang.
    Modular AC unification of higher-order patterns, Proceedings of the First International Conference on Constraints in Computational Logics, Munich, Lecture Notes in Computer Science 845, (Springer, Berlin, 1994) 105-120.
  2. Alberto Pravato.
    Structured unification algorithms for typed rewriting systems, Technical Report, Department of Computer Science. University of Turin, 1996.
  3. Zhenyu Qian and Kang Wang.
    Modular higher-order equational preunification, Journal of Symbolic Computation, 22, 4 (1996) 401-424.

Section 4.1.1 Higher-Order Term Rewriting Systems

  1. Serge Autexier.
    Hierarchical Contextual Reasoning, Dr.-Ing. Dissertation, Univesität des Saarlandes, Saarbrücken, Germany, 2003, xvi+229pp.
  2. Jürgen Avenhaus and Carlos Loría-Sáenz.
    Higher-order conditional rewriting and narrowing, Proceedings of the First International Conference on Constraints in Computational Logics, Munich, Lecture Notes in Computer Science 845, (Springer, Berlin, 1994), 269-284.
  3. Gilles Barthe, Horatiu Cirstea, Claude Kirchner and Luigi Liquori.
    Pure patterns type systems, Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, USA, (ACM, NewYork, 2003) 250-261.
  4. Eduardo Bonelli, Delia Kesner and Alejandro Ríos.
    A de Bruin notation for higher-order rewriting, Proceedings of the 11th International Conference on Rewriting Techniques and Applications (RTA'00), Lecture Notes in Computer Science 1833, (Springer, Berlin, 2000) 62-79, and Journal of Logic and Computation 2005 15(6):855-899.
  5. Christoph Benzmüller.
    Equality and extensionality in automated higher-order theorem proving, PhD thesis, Univesität des Saarlandes, Fachberiech Informatik, Saarbrücken, April, 1999.
  6. Clara Bertolissi, and Horatiu Cirstea and Claude Kirchner
    Translating combinatory reduction systems into the rewriting calculus, In Jean-Louis Giavitto and Pierre-Etienne Moreau, editors., Proceedings of RULE'03, 4th International Workshop on Rule-Based Programming, June 2003, Electronic Notes in Theoretical Computer Science 86 (2) (2003) 16-32.
  7. Frederic Blanqui
    Termination and Confluence of Higher-Order Rewrite Systems, Rewriting Techniques and Applications, 2000  Lecture Notes in Computer Science 1833, Lecture Notes in Computer Science (Springer, Berlin, 2000) 47-61.
  8. H.J. Sander Bruggink.
    Residuals in higher-order rewriting, in Robert Nieuwenhuis, Ed., Rewriting Techniques and Applications: 14th International Conference, RTA 2003, Lecture Notes in Computer Science 2706, (Springer, Berlin, 2003) 123-137.
  9. Horatiu Cirstea.
    The Rewriting Calculus: Theory and Applications (Calcul de réécriture: fondements et applications), Doctoral Thesis, Henri Poincaré University – Nancy 1, October 2000, viii+212pp.
  10. Horatiu Cirstea and Claude Kirchner.
    The rewriting calculus - Part I,  Logic Journal of the Interest Group in Pure and Applied Logics, 9(3):363--399, 2001.
  11. Horatiu Cirstea, Claude Kirchner and Luigi Liquori.
    Rewriting calculus with(out) types. In Fabio Gadducci and Ugo Montanari, editors, Proceedings of the fourth workshop on rewriting logic and applications, Pisa (Italy), September 2002. Electronic Notes in Theoretical Computer Science 71, 17 pp.
  12. Arie van Deursen and T.B. Dinesh.
    Origin tracking for higher-order rewriting systems, Higher-Order Algebra, Logic, and Term Rewriting, First International Workshop, HOA '93, Amsterdam, (Jan Heering, Karl Meinke, Bernhard Möller, and Tobias Nipkow, Eds.), Lecture Notes in Computer Science 816, (Springer, Berlin, 1994) 76-95.
  13. John Glauert and Zurab Khasidashvili.
    Relative normalization in orthogonal expression reduction systems, Proceedings of the Fourth International Workshop on Conditional and Typed Term Rewriting Systems, (CTRS '94), Lecture Notes in Computer Science 968, (Springer, Berlin, 1994) 144-165.
  14. John Glauert and Zurab Khasidashvili.
    Minimal and optimal relative normalization in orthogonal expression reduction systems, Technical Report SYS-C94-06, School of Information Systems, UEA Norwich.
  15. John Glauert, Richard Kennaway and Zurab Khasidashvili.
    Stable Results and relative normalization, Journal of Logic and Computation, 10, 3. Special Issue: Type Theory and Term Rewriting. F. Kamareddine and J. W. Klop, eds. Oxford University Press, 2000, 323-348.
  16. Jan Heering.
    Higher-Order Abstract Syntax and Higher-Order Term Rewriting  for Program Transformation
    Department of Software Engineering, CWI, Amsterdam, March 2004, 34 slides.
  17. Stefan Kahrs.
    Towards a domain theory for termination proofs, Proceedings of the International Conference on Rewriting Techniques and Applications, RTA-95, Kaiserslautern, Germany, (Jieh Hsiang, Ed.), Lecture Notes in Computer Science 914, (Springer, Berlin, 1995) 241-255.
  18. Zurab Khasidashvili.
    Context-sensitive conditional expression reduction systems, Proceedings of the International Workshop on Graph Rewriting and Computation, Electronic Notes in Theoretical Computer Science 2 (1995), 10 pp.
  19. Zurab Khasidashvili.
    On the longest perpetual reductions in orthogonal expression reduction systems, Theoretical Computer Science, to appear.
  20. Zurab Khasidashvili and Mizuhito Ogawa.
    Perpetuality and uniform normalization, Algebraic and Logic Programming, Sixth International Joint Conference, ALP '97 - HOA '97, Southampton, UK, September 1997, Lecture Notes in Computer Science 1298, (Springer, Berlin, 1997) 240-255.
  21. Zurab Khasidashvili, Mizuhito Ogawa and Vincent van Oostrom.
    Perpetuality and uniform normalization in orthogonal rewrite systems, Information and Computation, to appear.
  22. Jan Willem Klop, Vincent van Oostrom, and Femke van Raamsdonk.
    Combinatory reduction systems: introduction and survey, Theoretical Computer Science 121 (1993) 279-308.
  23. Richard Mayr and Tobias Nipkow.
    Higher-order rewrite systems and their confluence, Technical report TUM-I9433, Institut für Informatik, Technische Universität München, August 1994.
  24. Richard Mayr and Tobias Nipkow.
    Higher-order rewrite systems and their confluence, Theoretical Computer Science 192 (1998) 3-29.
  25. Micea Marin, Taro Suzuki and Tetsuo Ida
    Refinements of Lazy Narrowing for Left-Linear Fully-Extended Pattern Rewrite Systems, Technical Report ISE-TR-01-180, Institute of Information Sciences and Electronics, University of Tsukuba, Japan, 2001.
  26. Robert Muller and J. B. Wells.
    Two Applications of Standardization and Evaluation in Combinatory Reduction Systems, Boston College and Heriot-Watt University, 2000. Submitted for publication.
  27. Christian Prehofer.
    Solving Higher-Order Equations: From Logic to Programming, PhD Thesis, Technische Universität, München, November 1994, and a book published by Birkhäuser, Boston, 1997, 186 pp.
  28. Christian Prehofer.
    Higher-order narrowing, Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, Paris, (IEEE Computer Society, Washington, D.C., 1994) 507-516.
  29. Jaco van de Pol.
    Termination proofs for higher-order rewrite systems, Higher-Order Algebra, Logic, and Term Rewriting, First International Workshop, HOA '93, Amsterdam, (Jan Heering, Karl Meinke, Bernhard Möller, and Tobias Nipkow, Eds., Lecture Notes in Computer Science 816, (Springer, Berlin, 1994) 305-325.
  30. Jaco van de Pol.
    Termination of Higher-order Rewrite Systems, PhD thesis, Department of Philosophy, Utrecht University, The Netherlands, December 1996.
  31. Vincent van Oostrom and Femke van Raamsdonk.
    Comparing Combinatory Reduction Systems and higher-order rewrite systems, Higher-Order Algebra, Logic, and Term Rewriting, First International Workshop, HOA '93, Amsterdam, (Jan Heering, Karl Meinke, Bernhard Möller, and Tobias Nipkow, Eds.), Lecture Notes in Computer Science 816, (Springer, Berlin, 1994) 276-304.
  32. Vincent van Oostrom and Femke van Raamsdonk.
    Weak orthogonality implies confluence: the higher-order case, Logical Foundations of Computer Science, St Petersburg, Russia, July 1994, (Anil Nerode and Yuri V. Matiyasevich, Eds.), Lecture Notes in Computer Science 813, (Springer, Berlin, 1994) 379-392.
  33. Vincent van Oostrom.
    Confluence for Abstract and Higher-Order Rewriting, PhD thesis, Vrije Universiteit, Amsterdam, March 1994.
  34. Vincent van Oostrom.
    Confluence by developments and development closed critical pairs, Research Report, NTT BRL, Information Processing Principles Research Group, Japan.
  35. Vincent van Oostrom.
    Developing developments, Theoretical Computer Science 175 (1997) 159-181.
  36. Vincent van Oostrom.
    Finite family developments, Rewriting Techniques and Applications, Lecture Notes in Computer Science 1232, (Springer, Berlin, 1997) 308-322.
  37. Vincent van Oostrom.
    Sub-Birkhoff, Department of  Philosophy, Utrecht University,
  38. Femke van Raamsdonk.
    Confluence and Normalisation for Higher-Order Rewriting, PhD Thesis, Centrum voor Wiskunde en Informatica (CWI), Amsterdam, The Netherlands, May 1996.
  39. J.B. Wells and Robert Muller.
    Standardization and Evaluation in Combinatory Reduction Systems, Heriot-Watt University and Boston College, 2000. Submitted for publication.

Section 4.2 Higher-Order Unification

  1. Robert W. Hasker.
    The Replay of Program Derivations, PhD Dissertation, University of Illinois at Urbana-Champaign, 1995, 225 pp.
  2. John Lloyd.
    Declarative Programming in Escher, Technical Report CSTR-95-013, June 1995 (Revised August 1995), Department of Computer Science, University of Bristol.
  3. John Lloyd.
    Programming in an Integrated Functional and Logic Language, The Journal of Functional and Logic Programming, 1999, 3 (1999) 1-49.
  4. John Lloyd.
    Higher-order computational logic, in Antonis C. Kakas, Fariba Sadri and Robert A. Kowalski, Eds.,  Computational Logic: Logic Programming and Beyond : Essays in Honor of Robert A. Kowalski, (Springer, Berlin 2002) pp. 105-137.
  5. Satoshi Matsuoka.
    Towards a Higher Order Unification Based on Proof Nets, Workshop on Theories of Types and Proofs, (1997), a workshop of Theoretical Aspects of Computer Science (TACS 97).
  6. Paliath Narendran, Qing Guo, and D A Wolfram.
    Complexity of nilpotent unification and matching problems, Information and Computation 162, 1/2 (2000) 3-23.
  7. Christian Prehofer.
    Solving Higher-Order Equations: From Logic to Programming, PhD Thesis, Technische Universität, München, November 1994, and a book published by Birkhäuser, Boston, 1997, 186 pp.
  8. Manfred Schmidt-Schauß
    An Optimized Decision Algorithm for Stratified Context Unification, Fachbereich Informatik, Johann Wolfgang Goethe Universität, Germany, Frank-report-13, 2000, 19 pp.
  9. Manfred Schmidt-Schauß
    Decidability of bounded second order unification, Information and Computation 188, 2 (2003) 143-178.

Section 4.4 Decidability of Matching

  1. Richard J. Boulton.
    A restricted form of higher-order rewriting applied to an HDL semantics, Proceedings of the International Conference on Rewriting Techniques and Applications, RTA-95, Kaiserslautern, Germany, (Jieh Hsiang, Ed.), Lecture Notes in Computer Science, (Springer, Berlin, 1995) 309-323.
  2. Gilles Dowek.
    Third order matching is decidable, Annals of Pure and Applied Logic 69 (1994) 135-155; and Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, Amsterdam, (IEEE Computer Society, Washington, D.C., 1992) 2-10. (Cites my PhD Dissertation.)
  3. Gilles Dowek.
    Higher-order unification and matching, Chapter 16 of Handbook of Automated Reasoning, (Alan Robinson and Andrei Voronkov, Eds.), (Elsevier, Amsterdam, 2001) 1009-1062. (Cites my PhD Dissertation.)
  4. Gérard Huet
    Higher Order Unification 30 years later. Proceedings, 15th International Conference TPHOLs 2002. Eds V. Carreño, C. Muñoz and S. Tahar. Lecture Notes in Computer Science 2410, (Springer, Berlin, 2002) 3-12. (Cites my PhD Dissertation.)
  5. Matthias Neubauer and Peter Thiemann
    Type classes with more higher order polymorphism, SIGPLAN International Conference on Functional Programming, (ACM, 2002) 179-190.
  6. Oege de Moor and Ganesh Sittampalam.
    Higher order matching for program transformation, Functional and Logic Programming: Ninth Fuji International Symposium, FLOPS '99, Lecture Notes in Computer Science 1722, (Springer, Berlin, 1999) 209-224.
  7. Oege de Moor and Ganesh Sittampalam.
    Higher order pattern matching for automatically applying fusion transformations, Programs as Data Objects, Second Symposium, 2001, Lecture Notes in Computer Science 2053 (Springer, Berlin, 2001) 218-237.
  8. Christian Prehofer.
    Solving Higher-Order Equations: From Logic to Programming, PhD Thesis, Technische Universität, München, November 1994, and a book published by Birkhäuser, Boston, 1997, 186 pp.
  9. Christian Prehofer.
    Decidable higher-order unification problems, Proceedings of the Twelfth Conference on Automated Deduction, Nancy, Lecture Notes in Artificial Intelligence 814, (Springer, Berlin, 1994) 635-649.
  10. Manfred Schmidt-Schauß
    Decidability of arity bounded higher order matching,
    Proceedings of CADE-19,  Lecture Notes in Computer Science, (Springer, Berlin, 2003), 15 pages
  11. Manfred Schmidt-Schauß and Klaus U. Schulz
    Decidability of bounded higher-order unification, Journal of Symbolic Computation, 40, 2 (August 2005) 905-954.
  12. Aleksy Schubert.
    Linear interpolation for the higher-order matching problem, TAPSOFT '97: Theory and Practice of Software Development, Lille, France, Lecture Notes in Computer Science 1214, (Springer, Berlin, 1997) 441-452. (Cites my PhD Dissertation)
  13. Aleksy Schubert.
    Algebraic Higher-Order Matching, Technical Report of Institute of Informatics, Warsaw University, TR 02-02 (267), 10 February 2002.
  14. Jan Springintveld.
    Algorithms for Type Theory, PhD thesis, Department of Philosophy, Utrecht University, The Netherlands, 1995.
  15. Jan Springintveld.
    Third-order matching in the polymorphic lambda calculus, Higher-Order Algebra, Logic, and Term Rewriting, Lecture Notes in Computer Science 1074, (Springer, Berlin, 1995) 221-237.
  16. Sergei Vorobyov,
    The "hardest" natural decidable theory, Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw, 29 June to 2 July 1997, (IEEE Computer Society, Washington, D.C., 1997) 294-305.
  17. Sergei Vorobyov,
    Third order matching in lambda ->-Curry is undecidable, Technical report MPI-I-97-2-006, May 1997, Max-Planck Institüt für Informatik, Saarbrücken, Germany.

Section 4.4.4 Plotkin-Statman Conjecture

  1. Ralph Loader.
    The undecidability of lambda-definability, in: C. Anthony Anderson and M. Zeleny, Eds., Logic, Meaning and Computation: Essays in Memory of Alonzo Church, (Kluwer, Amsterdam, 2001) 331-342.
  2. Richard Statman and Gilles Dowek.
    On Statman's Finite Completeness Theorem, Technical Report CMU-CS-92-152, School of Computer Science, Carnegie Mellon University, 1 June 1992. (Cites my PhD Dissertation.)

Section 4.4.5 Decidable Matching Problems

  1. Sergei Vorobyov, The "hardest" natural decidable theory, Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw, 29 June to 2 July 1997, (IEEE Computer Society, Washington, D.C., 1997) 294-305.
  2. ToMasz Wierzbicki.
    Complexity of the higher-order matching, In Harald Ganzinger, editor, Automated Deduction - CADE-16: Sixteenth International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 1632 (Springer, Berlin, 1999) 82-96.

Section 4.4.6 Regular Unification Problems

  1. Marek Zaionc.
    Lambda definability is decidable for second order types and for regular third order types, Technical Report 95-24, Department of Computer Science, State University of New York at Buffalo, 1995.

Chapter 5 Higher-Order Logic Programming

  1. Manuel M. T. Chakravarty, Yike Guo, Martin Köhler and Hendrik Lock.
    Goffin: Higher-order functions meet concurrent constraints, Science of Computer Programming (1998) 30(1-2):157-199.
  2. Mario Rodríguez-Artalejo.
    The challenge of declarative programming, in: John W. Lloyd, Ed., Logic Programming: Proceedings of the 1995 International Symposium, (MIT Press, 1995)  pp. 629-630.

Section 5.1 Higher-Order Equational Resolution

  1. Peter B. Andrews.
    Classical type theory, in: Alan Robinson and Andrei Voronkov, Eds., Handbook of Automated Reasoning, (Elsevier Science, Amsterdam, 2001) pp. 965-1007.
  2. Christoph Benzmüller.
    Extensional higher-order paramodulation and RUE-resolution, In Harald Ganzinger, editor, Automated Deduction - CADE-16: Sixteenth International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 1632 (Springer, Berlin, 1999) 399-413.
  3. Christoph Benzmüller.
    An adaptation of paramodulation and RUE-resolution to higher-order logic, SEKI Report SR-98-07, Universität des Saarlandes, Saarbrücken, Germany, 1998.
  4. Christoph Benzmüller.
    Equality and extensionality in automated higher-order theorem proving, PhD thesis, Univesität des Saarlandes, Fachberiech Informatik, Saarbrücken, April, 1999.
  5. Christoph Benzmüller.
    Comparing approaches to resolution based higher-order theorem proving, Synthese, Volume 133, Issue 1-2, October - November 2002, pages 203-235.
  6. Christoph Benzmüller and Manfred Kerber.
    A challenge for mechanized deduction,     Proceedings of IJCAR Workshop on Future Directions in Automated Reasoning; editor: Manfred Kerber, (2001) pages 13-24.