3 Summary & Materials

This page will list students’ summaries and (links to) reading materials.

3.1 Full Abstraction: From PCF to SPCF

Robin Milner. Fully abstract models of typed lambda calculi. Theoretical Computer Science, 4(1), February 1977, pages 1-22.

Gordon Plotkin. LCF considered a programming language. Theoretical Computer Science, 5(3), December 1977, pages 223-256.

Gerard Berry and Pierre-Louis Curien. Sequential algorithms on concrete data structures. Theoretical Computer Science, 20(3), July 1982, pages 265-321.

Robert Cartwright, Pierre-Louis Curien, Matthias Felleisen. Information and Computation, 111(2), June 1994, pages 297-401.

3.2 Programming Languages and Calculi

Gordon Plotkin. Call-by-name, call-by-value, and the lambda calculus. Theoretical Computer Science, 1975, pages 125-159.

Matthias Felleisen, Daniel Friedman, Eugene Kohlbecker, and Bruce Duba. Reasoning with continuations. Logic in Computer Science, 1986, pages 314-325. (I cannot find an on-line link.)

Matthias Felleisen, Daniel Friedman. Control operators, the SECD machine and the lambda calculus. Formal Description of Programming Concepts, 1986, pages 193-217.

Matthias Felleisen, Daniel Friedman. A calculus of assignments in higher-order languages. Principles of Programming Languages, 1986, pages 314-325

Matthias Felleisen, Robert Hieb. A calculus of assignments in higher-order languages. Theoretical Computer Science, 1992, pages 235-271

3.3 From Encapsulation to Ownership

John C. Reynolds. Syntactic control of interference. Principles of Programming Languages, 1978, pages 39-46.

John Hogg. Islands: aliasing protection in object-oriented languages. Object-oriented Programming Systems Languages and Applications, 1991, pages 271-285.

David G. Clarke, John M. Potter, and James Noble. Ownership types for flexible alias protection. Object-oriented Programming Systems Languages and Applications, 1998, pages 48-64.

Christian Grothoff, Jens Palsberg, and Jan Vitek. Encapsulating objects with confined types. Transactions on Programming Languages and Systems, 29(6), October 2007.

3.4 Garbage Collection vs Manual Allocation

Henry Lieberman and Carl Hewitt. A real-time garbage collector based on the lifetimes of objects. MIT version Communications of the ACM, Volume 26 Issue 6, June 1983, pages 419-429.

Benjamin Zorn. The measured cost of conservative garbage collection. University of Colorado at Boulder Technical Report CU-CS-573-92. April, 1992. TR Software—Practice & Experience, Volume 23 Issue 7, July 1993, pages 733-756.

William D Clinger and Lars Hansen. Generational garbage collection and the radioactive decay model. In the Proceedings of the 1997 ACM Conference on Programming Language Design and Implementation, June 1997, pages 97-108.

William D Clinger and Fabio V Rojas. Linear combinations of radioactive decay models for generational garbage collection. In Science of Computer Programming, Volume 62, Issue 2, 1 October 2006, pages 184-203.

Felix S Klock II and William D Clinger. Bounded-latency regional garbage collection. Proceedings of the 2011 Dynamic Languages Symposium (DLS 2011), 24 October 2011, pages 73-83.

3.5 Higher-order Flow Analysis

3.6 Logical Relations: Stepping Beyond Toy Languages

Andrew Pitts and Ian Stark. Operational reasoning for functions with local state. Higher-Order Operational Techniques in Semantics (HOOTS ’98), 1998, pages 227-274.

Andrew Appel and David McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Transactions on Programming Languages and Systems 23 (5), September 2001, pages 657-683.

Amal Ahmed. Semantics of Types for Mutable State. Ch. 2, 3, 4. Ph.D. thesis, Princeton University, Princeton NJ, Nov. 2004. Tech Report TR-713-04.

Amal Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. European Symposium on Programming (ESOP ’06), March 2006, pages 69-83.

Amal Ahmed, Derek Dreyer, and Andreas Rossberg. State-Dependent Representation Independence. Principles of Programming Languages (POPL ’09), January 2009, pages 340-353.

3.7 Analysis-Based Program Transformation

Olin Shivers. The Semantics of Scheme Control-Flow Analysis. Conference on Programming Language Design and Implementation, June, 1991, pages 190-198.

Mitch Wand and Paul Steckler. Selective and Lightweight Closure Conversion. Conference on Principles of Programming Languages, January, 1994, pages 435-445.

Mitch Wand and Igor Siveroni. Constraint Systems for Useless Variable Elimination. Conference on Principles of Programming Languages, January, 1999, pages 291-302.

Mitch Wand and Will Clinger. Set Constraints for Destructive Array Update Optimization. International Conference on Computer Languages, 1998, pages 184–195.

Christos Dimoulas and Mitch Wand. The Higher-order Aggregate Update Problem. Verification, Model Checking, and Abstract Interpretation, 2009, pages 44-58.

3.8 Refinement Types

Noam Zeilberger. Principles of type refinement. Lectures Notes. Oregon Programming Language Summer School, 2016.

Freeman, Tim, and Frank Pfenning. Refinement types for ML. Programming Language Design and Implementation, 1991, pages 268-277.

Xi, Hongwei, and Frank Pfenning. Dependent types in practical programming. Principles of Programming Languages, 1999, pages 214-227.

Flanagan, Cormac. Hybrid type checking. Transactions on Programming Languages, 2010, 32(6), pages 1-34.

Xi, Hongwei. Dependent ML: an approach to practical programming with dependent types. Journal of Functional Programming. 17(2): 215-286, 2007.

Rondon, Patrick M., Ming Kawaguci, and Ranjit Jhala. Liquid Types. Programming Language Design and Implementation, 2008, pages 158-169.

3.9 Typed Directed Compilation

Xavier Leroy. Unboxed objects and polymorphic typing. Principles of Programming Languages, 1992, pages 177-188.

Greg Morrisett. Compiling with types.

Xavier Leroy. An overview of Types in Compilation. Workshop Types in Compilation, Lecture Notes in Computer Science, 1998, pages ??.

Greg Morrisett and Robert Harper. Typed Closure Conversion for Recursively-Defined Functions. Electronic Notes in Theoretical Computer Science, 1998, 10, pages 230-241.

David Tarditi, Greg Morrisett, Perry Cheng,. Chris Stone, Bob Harper. and Peter Lee. TIL: A Type-Directed Optimizing Compiler for ML. Programming Language Design and Implementation, 1996, pages 181-192.

3.10 Type-directed Compilation
with Dependent Types

George Necula and Peter Lee. The design and implementation of a certifying compiler. Programming Languages and Implementation, 1998, pages 333–344.

Gilles Barthe, John Hatcliff, and Morten Heine B Sorensen. CPS translations and applications: the cube and beyond. Higher-Order and Symbolic Computation, 1999, 12(2), pages 125–170.

Hongwei Xi and Robert Harper. A Dependently Typed Assembly Language. International Conference on Functional Programming, 2001, pages 169–180.

Hugo Herbelin. On the degeneracy of $\Sigma$-types in presence of computational classical logic. International Conference on Typed Lambda Calculi and Applications, 2005, pages 209–220.

Juan, Chen, Ravi Chugh, and Nikhil Swamy. Type-preserving Compilation of End-to-end Verification of Security Enforcement. Programming Language Design and Implementation, 2010, pages 412–423.

3.11 Refactoring

Frank Tip, Adam Kiezun, Dirk Bäumer. Refactoring for generalization using type constraints. OOPSLA 2003, pages 13-26.

Robert M. Fuhrer, Frank Tip, Adam Kiezun, Julian Dolby, Markus Keller. Efficiently refactoring java applications to use generic libraries. ECOOP 2005, pages 71-96.

Max Schäfer, Torbjörn Ekman, Oege de Moor. Sound and extensible renaming for Java. OOPSLA 2008, pages 277-294.

Friedrich Steimann, Andreas Thies. From public to private to absent: Refactoring Java programs under constrained accessibility. ECOOP 2009, pages 419-443.

Max Schäfer, Andreas Thies, Friedrich Steimann, Frank Tip. A comprehensive approach to naming and accessibility in refactoring Java programs. IEEE Trans. Software Eng. 38(6), 2012, pages 1233-1257.

3.12 Conversational Context & Concurrency

P. Brinch Hansen. Monitors and Concurrent Pascal: a personal history. History of Programming Languages II. SIGPLAN Notices, 1993, 28(3), pages 1–35. (also available here)

C. Hewitt, P. Bishop, and R. Steiger. A universal modular ACTOR formalism for artificial intelligence. International Joint Conference on Artificial Intelligence, 1973, pages 235–245. (also available here)

G. A. Agha. Actors: a model of concurrent computation in distributed systems. Technical Report 844. MIT Artificial Intelligence Laboratory, June 1985.

C. Fournet and G. Gonthier. The join calculus: a language for distributed mobile programming. Applied Semantics Summer School, September 2000, Caminha, Portugal.

N. J. Carriero, D. Gelernter, T. G. Mattson, and A. H. Sherman. The Linda alternative to message-passing systems. Parallel Comput., 20(4) pages 633–655, 1994.

3.13 Type Inference in Stack-based
Programming Languages

J. Poial. Algebraic specification of stack effects. Forth Dimensions, XVI(18_20).

J. Poial. Multiple stack effects for Forth programs. Euro Forth 1991

B. Stoddart & P.J. Knaggs. Type inference in stack based languages. Formal Aspects of Computing, 1992, pages 1-11.

C. Okasaki. Techniques for embedding post-fix languages in Haskell. cite 4

C. Diggins. Typing functional stack based languages. Unpublished manuscrtip, 2007.

A. Saabas & T. Uustalu. Type systems for optimizing stack-based code. Byte Code, 2007, pages 1-16. (See Electronic Notes in Theoretical Computer Science.)

3.14 Tracing JITs for Dynamic Languages

Vasanth Bala, Evelyn Duesterwald, and Sanjeev Banerjia. Dynamo: a transparent dynamic optimization system. Programming Language Design and Implementation, 2000, pages 1-12.

Andreas Gal and Michael Franz Incremental dynamic code generation with trace trees. Technical Report ICS-TR-06-16, University of California, Irvine, 2006.

Andreas Gal, Brendan Eich, Mike Shaver, David Anderson, David Mandelin, Mohammad R. Haghighat, Blake Kaplan, Graydon Hoare, Boris Zbarsky, Jason Orendorff, Jesse Ruderman, Edwin Smith, Rick Reitmaier, Michael Bebenita, Mason Chang, and Michael Franz. Trace-based just-in-time type specialization for dynamic languages. Programming Language Design and Implementation, 2009, pages 465-478.

Carl Friedrich Bolz, Antonio Cuni, Maciej Fijałkowski, and Armin Rigo. Tracing the meta-level: PyPy’s tracing JIT compiler. Implementation, Compilation, Optimization of Object-Oriented Languages and Programming Systems, 2009, pages 18-25.

Michael Bebenita, Florian Brandner, Manuel Fahndrich, Francesco Logozzo, Wolfram Schulte, Nikolai Tillmann, and Herman Venter. SPUR: a trace-based JIT compiler for CIL. Object-Oriented Programming, Systems, Languages and Applications 2010, pages 708-725.

Håkan Ardö, Carl Friedrich Bolz, and Maciej Fijałkowski Loop-aware optimizations in PyPy’s tracing JIT. Dynamic Languages Symposium (DLS), 2012, pages 63-72.

3.15 From PE to a JITs

Gregory T. Sullivan. Dynamic partial evaluation. Programs as Data Objects. Springer Berlin Heidelberg, 2001. 238-256.

Carl Friedrich Bolz, Antonio Cuni, Maciej Fijałkowski, and Armin Rigo. Tracing the meta-level: PyPy’s tracing JIT compiler. Implementation, Compilation, Optimization of Object-Oriented Languages and Programming Systems, 2009, pages 18-25.

Thomas Würthinger, Christian Wimmer, Andreas Wöß, Lukas Stadler, Gilles Duboscq, Christian Humer, Gregor Richards, Doug Simon, Mario Wolczko. One VM to rule them all. Onward! New Ideas, New Paradigms, and Reflections on Programming & Software, 2013, pages 187-204.

3.16 Datalog for Static Analysis

Stefano Ceri, Georg Gottlob, and Letizia Tanca. What you always wanted to know about datalog (and never dared to ask). IEEE Transactions on Knowledge and Data Engineering, 1989.

Aβman, Uwe. On edge addition rewrite systems and their relevance to program analysis. International Workshop on Graph Gramars and Their Application to Computer Science, 1994, pages 321-335

Thomas Reps Demand interprocedural program analysis using logic databases. Application of Logic Databases, 1995, pages 163-196.

Monica Lam, John Whaley, V. Benjamin Livshits, Michael C. Martin, Dzintars Avots, Michael Carbin, Christopher Unkel. Context-sensitive program analysis as database queries. Principles of Database Systems, 2005,pages 1-12.

Martin Bravenboer and Yannis Smaragdakis Strictly declarative specifications of sophisticated points-to analyses. Object Oriented Programming Systems Languages and Applications, 2009, pages 243-262.

3.17 Categorical Semantics of
Untyped Languages

Dana Scott. Relating theories of the lambda calculus. To H.B. Curry. Essays on Combinatory Logic, Lambda Calculus and Formalism. 1980, pages 403-450.

C.P.J. Koymans. Models of the lambda calculus. Information and Control, 52(3), 1982, pages 306-332.

Susumu Hayashi. Adjunctions of semi-functors. Theoretical Computer Science, 41(1), 1985, pages 95-104.

J. Lambek & P. Scott. Introduction to Higher Categorical Logic. Cambridge University Press, 1986.

R. Hoofman & I. Moerdijk. A remark on the theory of semi-functors. Mathematical Structures in Computer Science, 5(1), 1995, pages 1-8.

3.18 Linear Types for Low-level Languages

Yves Lafont. The linear abstract machine. Theoretical Computer Science, 59(1–2), 1988, pages 157–180.

Henry Baker. Lively linear Lisp – “look ma, no garbage!” SIGPLAN Notices, 27(8), 1992, pages 89 - 98.

Jawahar Chirimar, Carl A. Gunter, Jon G. Riecke. Reference counting as a computational interpretation of linear logic. Journal of Functional Programming, 6(2), 1996, pages 195-244.

Martin Hofmann. A type system for bounded space and functional in-place update–extended abstract. European Symposium on Programming, 2000, pages 165-179.

3.19 Probably Something

D Wingate, A Stuhlmueller, ND Goodman. Lightweight implementations of probabilistic programming languages via transformational compilation. International Conference on Artificial Intelligence and Statistics, 2011, pages 770-778.

Vikash Mansinghka, Daniel Selsam, Yura Perov. Venture: a higher-order probabilistic programming platform with programmable inference. arXiv.

L Yang, P Hanrahan, ND Goodman. Generating efficient mcmc kernels from probabilistic programs. International Conference on Artificial Intelligence and Statistics, 2014, pages 1068-1076.

JW van de Meent, H Yang, V Mansinghka, F Wood. Particle gibbs with ancestor sampling for probabilistic programs. International Conference on Artificial Intelligence and Statistics, 2015, pages 986-994.

D Ritchie, A Stuhlmüller, ND Goodman. C3: lightweight incrementalized MCMC for probabilistic programs using continuations and callsite caching. International Conference on Artificial Intelligence and Statistics, 2016, pages 28-37.

3.20 Functional Reactive Programming

Conal Elliott and Paul Hudak. Functional reactive animation. International Conference on Functional Programming, 1997, pages 263 - 273.

Zhanyong Wan and Paul Hudak. Functional reactive programming from first principles. Programming Language Design And Implementation, 2000, pages 242-252.

Conal Elliott. Functional implementations of continuous modeled animation. International Symposium on Principles of Declarative Programming, 2006, pages 284-299.

Gregory H. Cooper and Shriram Krishnamurthi. Embedding dynamic dataflow in a call-by-value language. European Symposium on Programming Languages and Systems, 2006, pages 294-308.

3.21 Soft Typing

3.22 No good answers: Gradually typed
object-oriented languages

G. Bierman, E. Meijer, and M. Torgersen. Adding dynamic types to C#. European Conference on Object-Oriented Programming, 2010, pages 76-100.

Bard Bloom, John Field, Nathaniel Nystrom, Johan Östlund, Gregor Richards, Rok Strnisa, Jan Vitek, and Tobias Wrigstad. Thorn: robust, concurrent, extensible scripting on the JVM. Object-oriented Programming Systems Languages and Applications, 2009, Pages 117-136.

Esteban Allende, Oscar Callaú, Johan Fabry, Éric Tanter, Marcus Denker. Gradual typing for Smalltalk. In Science of Computer Programming, 2014, 96(1), pages 52–69.

Michael M. Vitousek, Andrew M. Kent, Jeremy G. Siek, and Jim Baker. Design and evaluation of gradual typing for python. Dynamic Languages Symposium, 2014, pages 45-56.

Asumu Takikawa, Daniel Feltey, Ben Greenman, Max S. New, Jan Vitek, and Matthias Felleisen. Is sound gradual typing dead?. Principles of Programming Languages, 2016, pages 456-468.

3.23 No good answers (2): Shared Memory
Concurrency and Language Designs

Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers 1979, 28(9): 690-691.

Hans-Juergen Boehm. Threads cannot be implemented as a library. PLDI 2005, 261-268.

Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, Magnus O. Myreen. X86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM 2010, 53(7): 89-97.

Jaroslav Sevcík. Safe optimisations for shared-memory concurrent programs. PLDI 2011, 306-316.

Hans-Juergen Boehm, Sarita V. Adve. Foundations of the C++ concurrency memory model. PLDI 2008, 68-78.

Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, Francesco Zappa Nardelli. Common compiler optimisations are invalid in the C11 memory model and what we can do about it. POPL 2015, 209-220.