Great Works in Programming Languages

Blog posts.md

• http://blog.felipe.rs/2017/07/07/where-do-type-systems-come-from/
• http://tomasp.net/academic/papers/against-types/
• Against a universal definition of ‘type’
• The Triumph of Types: Principia Mathematica’s Impact on Computer Science
• Function and Concept
• https://www.cs.uoregon.edu/research/summerschool/summer15/curriculum.html

Great Works in Programming Languages.md

original version by Benjamin C. Pierce

The greatest of the great (mentioned by many people):

• C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580 and 583, October 1969.
• Peter J. Landin. The next 700 programming languages. Communications of the ACM, 9(3):157-166, March 1966.
• Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, August 1978.
• Gordon Plotkin. Call-by-name, call-by-value, and the λ-calculus. Theoretical Computer Science, 1:125-159, 1975.
• John C. Reynolds. Towards a theory of type structure. In Colloque sur la Programmation, Paris, France, volume 19 of Lecture Notes in Computer Science, pages 408-425. Springer-Verlag, 1974.

Pretty great works (mentioned by multiple people):

• Luca Cardelli. A semantics of multiple inheritance. In G. Kahn, D. MacQueen, and G. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 51-67. Springer-Verlag, 1984. Full version in Information and Computation, 76(2/3):138-164, 1988.
• Luis Damas and Robin Milner. Principal type schemes for functional programs. In ACM Symposium on Principles of Programming Languages (POPL), Albuquerque, New Mexico, pages 207-212, 1982.
• Edsger W. Dijkstra. Recursive programming. In Saul Rosen, editor, Programming Systems and Languages, chapter 3C, pages 221-227. McGraw-Hill, New York, 1960.
• Edsger W. Dijkstra. Go to statement considered harmful. 11(3):147-148, March 1968.
• William A. Howard. The formulas-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479-490. Academic Press, 1980. Reprint of 1969 article.
• Robert Kowalski. Predicate logic as programming language. In IFIP Congress, pages 569-574, 1974. Reprinted in Computers for Artificial Intelligence Applications, (eds. Wah, B. and Li, G.-J.), IEEE Computer Society Press, Los Angeles, 1986, pp. 68-73.
• Peter J. Landin. The mechanical evaluation of expressions. Computer Journal, 6(4):308-320, January 1964.
• John McCarthy. Recursive functions of symbolic expressions and their computation by machine, part I. Communications of the ACM, 3(4):184-195, April 1960.
• Eugenio Moggi. Computational lambda-calculus and monads. In IEEE Symposium on Logic in Computer Science (LICS), Asilomar, California, pages 14-23, June 1989. Full version, titled Notions of Computation and Monads, in Information and Computation, 93(1), pp. 55-92, 1991.
• Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System-F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):527-568, May 1999.
• George C. Necula. Proof-carrying code. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France, pages 106-119, January 1997.
• Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223-255, 1977.
• Gordon D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981.
• Guy Lewis Steele, Jr. RABBIT: A compiler for SCHEME. Technical Report AITR-474, MIT Artificial Intelligence Laboratory, May 6 1978.

A great many great works (mentioned at least once):

• C. Boehm and G. Jacopini. Flow diagrams, Turing machines, and languages with only two formation rules. Communications of the ACM, 9(5):366-371, 1966.
• Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56-68, 1940.
• Alonzo Church. The Calculi of Lambda Conversion. Princeton University Press, 1941.
• Haskell B. Curry and Robert Feys. Combinatory Logic, volume 1. North Holland, 1958. Second edition, 1968.
• O. J. Dahl and K. Nygaard. SIMULA-An ALGOL-based simulation language. Communications of the ACM, 9(9):671-678, September 1966.
• Matthias Felleisen. On the expressive power of programming languages. Science of Computer Programming, 17(1-3):35-75, December 1991.
• Andrzej Filinski. Representing layered monads. In ACM Symposium on Principles of Programming Languages (POPL), San Antonio, Texas, pages 175-188, New York, NY, 1999.
• Robert W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19-32, Providence, Rhode Island, 1967. American Mathematical Society.
• Michael J. Gordon, Robin Milner, F. Lockwood Morris, Malcolm Newey, and Christopher P. Wadsworth. A metalanguage for interactive proof in LCF. Internal Report CSR-16-77, University of Edinburgh, Edinburgh, Scotland, September 1977.
• C. A. R. Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39-45, January 1971.
• C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666-677, August 1978. Reprinted in "Distributed Computing: Concepts and Implementations" edited by McEntire, O'Reilly and Larson, IEEE, 1984.
• Thomas Johnsson. Lambda lifting: transforming programs to recursive equations. In Functional programming languages and computer architecture. Proc. of a conference (Nancy, France, Sept. 1985), pages 190-203, New York, NY, USA, 1985. Springer-Verlag Inc.
• Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall International, Hemel Hempstead, Hertfordshire, UK, 1993.
• G. Kahn. The semantics of a simple language for parallel programming. In J. L. Rosenfeld, editor, Information processing, pages 471-475, Stockholm, Sweden, Aug 1974. North Holland, Amsterdam.
• Gilles Kahn. Natural semantics. In Franz-Josef Brandenburg, Guy Vidal-Naquet, and Martin Wirsing, editors, Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS), volume 247 of Lecture Notes in Computer Science, pages 22-39. Springer-Verlag, 1987.
• Donald E. Knuth. Structured programming with go to statements. Computing Surveys, 6(4):261-301, 1974.
• Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.
• Peter Naur et al. Revised report on the algorithmic language ALGOL 60. Communications of the ACM, 6(1):1-17, January 1963.
• John C. Reynolds. Types, abstraction, and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, Paris, France, pages 513-523. Elsevier, 1983.
• John C. Reynolds. Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation, 11(4):363-397, 1998. Reprinted from the proceedings of the 25th ACM National Conference (1972), with a foreword.
• Dana Scott. Continuous lattices. In F. W. Lawvere, editor, Toposes, Algebraic Geometry, and Logic, number 274 in Lecture Notes in Mathematics, pages 97-136. Springer-Verlag, 1972.
• Dana Scott and Christopher Strachey. Toward a mathematical semantics for computer languages. Programming Research Group Technical Monograph PRG-6, Oxford Univ. Computing Lab., 1971.
• Dana S. Scott. Outline of a mathematical theory of computation. Technical Monograph PRG-2, Oxford University Computing Laboratory, Oxford, England, November 1970.
• Brian Cantwell Smith. Reflection and semantics in lisp. In ACM Symposium on Principles of Programming Languages (POPL), Salt Lake City, Utah, pages 23-39, January 1984.
• Christopher Strachey. Towards a formal semantics. In Formal Language Description Languages for Computer Programming, pages 198-220. North Holland, 1966.
• Christopher Strachey. Fundamental concepts in programming languages. Lecture Notes, International Summer School in Computer Programming, Copenhagen, August 1967. Reprinted in Higher-Order and Symbolic Computation, 13(1/2), pp. 1-49, 2000.
• Christopher Strachey and Christopher P. Wadsworth. Continuations: A mathematical semantics for handling full jumps. Programming Research Group Technical Monograph PRG-11, Oxford Univ. Computing Lab., 1974. Reprinted in Higher-Order and Symbolic Computation, vol. 13 (2000), pp. 135-152.
• D. A. Turner. A new implementation technique for applicative languages. Software - Practice and Experience, 9(1):31-49, Jan 1979.
• David Ungar and Randall B. Smith. Self: The power of simplicity. Lisp and Symbolic Computation, 4(3):187-205, 1991.
• N. Wirth. The programming language Pascal (revised report). Technical report 5, Dept. Informatik, Inst. Für Computersysteme, ETH Zürich, Zürich, Switzerland, Jul 1973.
• Niklaus Wirth and C. A. R. Hoare. A contribution to the development of ALGOL. Communications of the ACM, 9(6):413-432, June 1966.
• Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38-94, November 1994.

JS Type System.md

• https://ac.els-cdn.com/S1571066105051340/1-s2.0-S1571066105051340-main.pdf?_tid=4200dd03-ed3e-4907-9527-21a54cd7333e&acdnat=1521328233_0b46115f1211f64e70acb56447aeb634
• https://courses.cs.washington.edu/courses/cse501/15sp/papers/ahn.pdf
• https://stackoverflow.com/questions/964910/is-javascript-an-untyped-language
• https://stackoverflow.com/questions/9154388/does-untyped-also-mean-dynamically-typed-in-the-academic-cs-world
• https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf
• https://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf
• http://publish.uwo.ca/~jbell/types.pdf

Other works about types.md

• Fundamental Concepts in Programming Languages, 1967
• On Understanding Types, Data Abstraction, and Polymorphism, 1985
• Type systems. Luca Cardelli, 1997
• Lambda Calculi with types, 1993 (Lambda Cube)
• Pure Type Systems for Functional Programming, 2003
• Propositions as Types

What type of thing is a type?.md

oritinal version by Ronald Garcia

• Types Are Not Sets by J.H. Morris, 1973
• A Theory of Type Polymorphism in Programming by R. Milner, 1978
• Types, Abstraction, and Parametric Polymorphism by J.C. Reynolds, 1983
• Co-induction in Relational Semantics by R. Milner and M. Tofte, 1988
• Typing First-class Continuations in ML by B.F. Duba, R. Harper, and D. MacQueen, 1990
• A Syntactic Approach to Type Soundness by A.K. Wright and M. Felleisen, 1992
• Semantics of Types for Mutable State by A.J. Ahmed, 2004