An Eclectic Bibliography on Programming Language Semantics

This collection consists of works on PL semantics currently of interest to me personally, and is not intended to be comprehensive, nor focused on a single perspective on semantics -- hence the description "eclectic". That said, many of the works included here are related to the approach to semantics presented in Felleisen et al's Semantics Engineering with PLT Redex. Other works which I have included, such as those related to denotational semantics, may still be of historical interest.

For the most part, I have included only works which are available online. The works below (and others) are available on the Readscheme.org website.

- Jim Bender (readscheme@gmail.com)

Foundational Papers
  • Peter J. Landin. The Mechanical Evaluation of Expressions. Computer Journal, 6:308-320, 1964. Available online: pdf.
  • John McCarthy. A Basis for a Mathematical Theory of Computation. In P. Braffort and D. Hirschberg, editors, Computer Programming and Formal Systems, pages 33-70. North Holland. 1963. Available online: pdf.
  • James H. Morris. Lambda-Calculus Models of Programming Languages. Ph.D. thesis. Massachussetts Institute of Technology, 1968. Available online: pdf.
  • Gordon D. Plotkin. Call-by-name, Call-by-value, and the λ Calculus. Theoretical Computer Science, 1:125-159, 1975. Available online: pdf.
  • Gordon D. Plotkin. LCF Considered as a Programming Language. Theoretical Computer Science, 5:223-255, 1977. Available online: pdf.
  • John C. Reynolds. Definitional Interpreters for Higher-order Programming Languages. 25th ACM National Conference. August 1972. Reprinted in Higher-Order and Symbolic Computation 11(4):363-–397, 1998. Available online: pdf. See also Reynolds' forward to HOSC reprint: pdf.
Reduction Semantics
  • Matthias Felleisen, Robert Bruce Findler and Matthew Flatt. Semantics Engineering with PLT Redex. MIT Press. 2009.
  • Matthias Felleisen, Daniel P. Friedman, Eugene Kohlbecker and Bruce Duba. Reasoning with Continuations. First Symposium on Logic in Computer Science. 1986. Technical report version available as TR-191, Indiana University. Available online: pdf.
  • Matthias Felleisen and Daniel P. Friedman. Control Operators, the SECD-machine, and the λ-Calculus. In Formal Description of Programming Concepts III. August 1986. Also available as the technical report TR-197, Indiana University. Available online: pdf.
  • Matthias Felleisen and Daniel P. Friedman. A Calculus for Assignments in Higher-Order Languages. Principles of Programming Languages (POPL'87). Also available as the technical report TR-202, Indiana University. Available online: pdf.
  • Matthias Felleisen, Daniel P. Friedman, Bruce F. Duba and John Merrill. Beyond Continuations. Technical report TR-216, Indiana University. February 1987. Available online: pdf.
  • Matthias Felleisen. Reflections on Landin's J-operator: A Partly Historical Note. Journal of Computer Languages, 12(3/4):197–207, 1987. Also available as the technical report TR-205, "A Final Scheme-Word on Landin's J-Operator", Indiana University. Available online: pdf.
  • Matthias Felleisen and Daniel P. Friedman. A Reduction Semantics for Imperative Higher-Order Languages. Conference on Parallel Architectures and Languages Europe (PARLE'87). June 1987. Also available as the technical report TR-218, Indiana University. Available online: pdf.
  • Matthias Felleisen, Daniel P. Friedman and Bruce F. Duba. Abstract Continuations: A Mathematical Semantics for Handling Full Functional Jumps. Lisp and Functional Programming (LFP'88). July 1988. Also available as the technical report TR-248, Indiana University. Available online: pdf.
  • Matthias Felleisen. The Calculi of Lambda-v-CS Conversion: A Syntactic Theory of Control And State in Imperative Higher-Order Programming Languages. Ph.D. Thesis. Computer Science Technical Report 226. August 1987. Available online: pdf.
  • Matthias Felleisen, Daniel P. Friedman, Eugene Kohlbecker and Bruce F. Duba. A Syntactic Theory of Sequential Control. Theoretical Computer Science, 52:205-237, 1987. Also available as the technical report TR-215, Indiana University. Available online: pdf.
  • Matthias Felleisen and Daniel P. Friedman. A Syntactic Theory of Sequential State. Theoretical Computer Science, 69:243-287, 1989. Also available as the technical report TR-230, Indiana University. Available online: pdf.
  • Matthias Felleisen and Robert Hieb. The Revised Report on the Syntactic Theories of Sequential Control and State. Theoretical Computer Science, 103:235-271, 1992 . Available online: pdf.
  • Andrew K. Wright and Matthias Felleisen. A Syntactic Approach to Type Soundness. Information and Computation, 115(1):38-94, 1994. Available online: pdf.
Examples
  • Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt and Robert Bruce Findler. Run Your Research: On the Effectiveness of Lightweight Mechanization. Principles of Programming Languages (POPL 2012). January 2012. Available online: pdf, redex models.
  • Casey Klein, Jay McCarthy, Steven Jaconette and Robert Bruce Findler. A Semantics for Context-Sensitive Reduction Semantics. Asian Symposium on Programming Languages and Systems (APLAS 2011). 2011. Available online: pdf, extended version, redex model.
  • Zena M. Ariola and Matthias Felleisen. The call-by-need lambda calculus. Journal of Functional Programming. 7:265-301, 1997. Available online: pdf.
  • Stephen Chang and Matthias Felleisen. The Call-by-need Lambda Calculus, Revisited. European Symposium on Programming. 2012. Available online: pdf.
  • Casey Klein, Matthew Flatt and Robert Bruce Findler. The Racket Virtual Machine and Randomized Testing. Unpublished. 2010. Available online: pdf, redex model.
  • Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. Blame for All. Principles of Programming Languages (POPL 2011). January 2012. Available online: pdf, redex model.
Inter-deriving Semantic Artifacts
  • Olivier Danvy and Lasse R. Nielsen. Defunctionalization at work. Principles and Practice of Declarative Programming (PPDP’01), September 2001. Extended version available as the research report BRICS RS-01-23. Available online: pdf.
  • Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A functional correspondence between evaluators and abstract  machines. Principles and Practice of Declarative Programming (PPDP’03). August 2003. Also available as the research report BRICS RS-03-13. Available online: pdf.
  • Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. From interpreter to compiler and virtual machine: a functional  derivation. Research Report BRICS RS-03-14. University of Aarhus. March 2003. Available online: pdf.
  • Olivier Danvy. A rational deconstruction of Landin’s SECD machine. Implementation and Application of Functional Languages, 16th  International Workshop, IFL’04. September 2004. Extended version available as the research report BRICS RS-03-33. Available online: pdf.
  • Olivier Danvy. On Evaluation Contexts, Continuations, and the Rest of the Computation. Continuations Workshop 2004 (CW04). January 2004. Available online: pdf.
  • Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A functional correspondence between call-by-need evaluators and lazy abstract machines. Information Processing Letters, 90(5):223–232. 2004. Extended version available as the technical report BRICS-RS-04-3. Available online: pdf.
  • Dariusz Biernacki and Olivier Danvy. From interpreter to logic engine by defunctionalization. Logic Based Program Synthesis and Transformation (LOPSTR 2003). August 2003. Also available as the research report BRICS RS-04-5. Available online: pdf.
  • Olivier Danvy and Lasse R. Nielsen. Refocusing in reduction semantics. Technical Report BRICS RS-04-26. University of Aarhus. November 2004. A preliminary version appears in proceedings of the Workshop on Rule-Based Programming (RULE 2001). Available online: pdf.
  • Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A functional correspondence between monadic evaluators and abstract machines for languages with computational effects. Theoretical Computer Science, 342(1):149–172, 2005. Extended version available as the research report BRICS RS-04-28. Available online: pdf.
  • Olivier Danvy. From reduction-based to reduction-free normalization. Workshop on Reduction Strategies in Rewriting and Programming (WRS'04). May 2004. Also available as the research report BRICS RS-04-30. Available online: pdf.
  • Małgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Computer Science, 1(2:5):1–39. November 2005. Also available as the research report BRICS RS-05-24. Available online: pdf.
  • Dariusz Biernacki. The Theory and Practice of Programming Languages with Delimited Continuations. PhD thesis, BRICS PhD School, University of Aarhus. December 2005. Available online: pdf.
  • Małgorzata Biernacka. A Derivational Approach to the Operational Semantics of Functional Languages. PhD thesis, BRICS PhD School, University of Aarhus. January 2006. Available online: pdf.
  • Olivier Danvy and Kevin Millikin. A rational deconstruction of Landin’s J operator. Research Report BRICS RS-06-17. University of Aarhus. December 2006. A preliminary version appears in the proceedings of the Workshop on the Implementation and Application of Functional Languages. Available online: pdf.
  • Małgorzata Biernacka and Olivier Danvy. A syntactic correspondence between context-sensitive calculi and abstract machines. Theoretical Computer Science, 375(1-3):76–108, 2007. Extended version available as the research report BRICS RS-05-38. Available online: pdf.
  • Małgorzata Biernacka and Olivier Danvy. A concrete framework for environment machines. ACM Transactions on Computational Logic, 9 (1):1–30, 2007. Extended version available as the research report BRICS RS-06-3. Available online: pdf.
  • Olivier Danvy and Kevin Millikin. A rational deconstruction of Landin’s J operator. Logical Methods in Computer Science, 4(4:12):1-67. November 2008. Available online: fulltext.
  • Olivier Danvy and Kevin Millikin. On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion. Information Processing Letters, 106(3):100–109, 2008. Extended version available as the technical report BRICS RS-07-16. Available online: pdf.
  • Olivier Danvy. From Reduction-based to Reduction-free Normalization. Summer School on Advanced Functional Programming (AFP08). May 2008. Available online: pdf.
  • Olivier Danvy and Kevin Millikin. Refunctionalization at work. Science of Computer Programming, 74(8):534-–549. 2009. Extended version available as the research report BRICS RS-08-04. Available online: pdf.
  • Olivier Danvy and Jacob Johannsen. Inter-deriving semantic artifacts for object-oriented programming. Workshop on Logic, Language, Information and Computation (WoLLIC 2008). July 2008. Extended version available as the research report BRICS RS-08-05. Available online: pdf.
  • Jacob Johannsen. An Investigation of Abadi and Cardelli's Untyped Calculus of Objects. Master's thesis. BRICS RS-08-06. University of Aarhus. June 2008. Available online: pdf.
  • Olivier Danvy. "Towards compatible and interderivable semantic specifications for the Scheme programming language, part I: abstract machines, natural semantics, and denotational semantics". 2008 Workshop on Scheme and Functional Programming. September 2008. Available online: pdf.
  • Małgorzata Biernacka and Olivier Danvy. "Towards compatible and interderivable semantic specifications for the Scheme programming  language, part II: reduction semantics and abstract machines". 2008 Workshop on Scheme and Functional Programming. September 2008.  Available online: pdf.
  • Olivier Danvy. Defunctionalized Interpreters for Programming Languages. International Conference on Functional Programming (ICFP08). September 2008. Available online: ACM Digital Library.
  • Ian Zerny. On Graph Rewriting, Reduction and Evaluation. Trends in Functional Programming Volume 10 (TFP 2009). 2009. Available online: pdf.
  • Olivier Danvy, Kevin Millikin, Johan Munk, and Ian Zerny. Defunctionalized Interpreters for Call-by-Need Evaluation. Functional and Logic Programming (FLOPS 2010). April 2010. Available online: pdf.
  • Olivier Danvy, Jacob Johannsen and Ian Zerny. A Walk in the Semantic Park. Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2011). January 2011. Available online: pdf.
  • Olivier Danvy, Kevin Millikin, Johan Munk, and Ian Zerny. On Inter-deriving Small-step and Big-step Semantics: A Case Study for Storeless Call-by-need Evaluation. Theoretical Computer Science, to appear 2012. Available online: pdf.
Research by Talcott and Mason
  • Carolyn Talcott. "The essence of Rum: A theory of the intensional and extensional aspects of Lisp-type computation". Ph.D. Thesis. Stanford University. August 1985. Available online: pdf.
  • Ian A. Mason. "The Semantics of Destructive Lisp". Ph.D. Thesis. Stanford University. 1986. Available online: pdf.
  • Carolyn Talcott. "Programming and Proving with Function and Control Abstractions". Stanford University. CS-TR-89-1288. October 1989. Available online: pdf.
  • Ian A. Mason and Carolyn L. Talcott. Inferring the Equivalence of Functional Programs that Mutate Data. Theoretical Computer Science, 105(2):167-215, 1992. Available online: pdf.
Early Works by Christopher Strachey, Dana Scott, and their Colleagues
  • Christopher Strachey. Fundamental Concepts in Programming Languages. Unpublished. 1967. Reprinted in Higher-Order and Symbolic Computing: pdf.
  • Dana Scott. Outline of a Mathematical Theory of Computation. 1970. Princeton University. Available online: pdf
  • Dana Scott. Outline of a Mathematical Theory of Computation. Technical monograph PRG-2. Oxford University. November 1970. Available online: pdf.
  • Dana Scott. The Lattice of Flow Diagrams. Technical monograph PRG-3. Oxford University. November 1970. Available online: pdf.
  • Dana Scott and Christopher Strachey. Toward a Mathematical Semantics for Computer Languages. Symposium on Computers and Automata. April 1971. Available online: pdf.
  • Dana Scott. Continuous Lattices. Technical monograph PRG-7. Oxford University. August 1971. Available online: pdf.
  • Dana Scott and Christopher Strachey. Toward a Mathematical Semantics for Computer Languages. Technical monograph PRG06. Oxford University. August 1971. Available online: pdf.
  • Christopher Strachey. The Varieties of Programming Language. Technical monograph PRG-10. Oxford University. March 1973. Available online: pdf.
  • Christopher Strachey and Christopher P. Wadsworth. Continuations: A Mathematical Semantics for Handling Full Jumps. Technical monograph PRG-11. Oxford University. January 1974. Available online: pdf. Reprinted in Higher-Order and Symbolic Computing (pdf). See also the forward by Peter Mosses (pdf).
  • Peter Mosses. The Mathematical Semantics of Algol 60. Technical Monograph PRG-12. Oxford University. January 1974. Available online: pdf. See also commentary by Peter Mosses (pdf).
  • Robert Milne. The Formal Semantics of Computer Languages and Their Implementations. Ph.D. thesis. Oxford University. 1974. Available online: pdf
  • Dana Scott. Data Types as Lattices. Technical monograph PRG-5. Oxford University. September 1976. Available online: pdf.
  • Joseph E. Stoy. The Congruence of Two Programming Language Definitions. Theoretical Computer Science, 13:151-174, 1981. Also available as technical monograph PRG-13, Oxford University. Available online: pdf.
Other Works
  • Peter J. Landin. The Next 700 Programming Languages. Communications of the ACM, 9(3):157-166, March 1966. Available online: pdf.
  • Peter J. Landin. A Generalization of Jumps and Labels. Report, UNIVAC Systems Programming Research, August 1965. Reprinted in Higher-Order and Symbolic Computing, 11(2):125-143, December 1998. Available online: pdf. See also Hayo Thielecke's forward to the HOSC reprint, An Introduction to Landin's "A Generalization of Jumps and Labels" (pdf).
  • John C. Reynolds. GEDANKEN: A Simple Typeless Language Which Permits Functional Data Structures and Coroutines. Technical report ANL-7621, Argonne National Laboratory. September 1969. Available online: pdf.
  • John C. Reynolds. GEDANKEN: A Simple Typeless Language Based on the Principle of Completeness and the Reference Concept. Communications of the ACM, 13(5):308-319, May 1970. Available online: pdf.
  • David A. Schmidt. Denotational Semantics: A Methodology for Language Development. 1986. Available online: pdf.
  • Michael J. Fischer. Lambda Calculus Schemata. Lisp and Symbolic Computing, 6:259-288, November 1993. Available online: pdf.
  • John Hatcliff and Olivier Danvy. Thunks and the λ-calculus. Journal of Functional Programming, 7(3):303-319. 1997. Available online: pdf. Expanded version available as the research report BRICS RS-97-7 (pdf).
Comments