A Classical Sequent Calculus with Dependent Types

Étienne Miquey. ACM Trans. Program. Lang. Syst. 41(2) (2019)

Only up to and including 2.5 and also 3.1

Paper (PDF)

To determine

To determine

To determine

To determine

To determine

To determine

To determine

Tracing the Meta-Level: PyPy's Tracing JIT Compiler

Carl Friedrich Bolz, Antonio Cuni, Maciej Fijalkowski and Armin Rigo. Proceedings of the 4th Workshop on the Implementation, Compilation, Optimization of Object-Oriented Languages and Programming Systems (2009)

Paper (PDF)

Block-Based Syntax from Context-Free Grammars

Mauricio Verano Merino and Tijs van der Storm. In: Proceedings of the 13th ACM SIGPLAN International Conference on Software Language Engineering (2020)

Paper (PDF)

The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects

Pierre-Marie Pédrot and Nicolas Tabareau. Proc. ACM Program. Lang. 4(POPL) (2020)

Paper (PDF)

The Size-Change Principle for Program Termination

Chin Soon Lee, Neil D. Jones and Amir M. Ben-Amram. Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2001)

Paper (PDF)

On Understanding Data Abstraction, Revisited

William R. Cook. Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications (2009)

Paper (PDF)

A Symmetric Lambda Calculus for Classical Program Extraction

Franco Barbanera and Stefano Berardi. Inf. Comput. 125(2) (1996)

We discuss Sections 1 and 2. Motivated participants can read 3 and 4. David would like to discuss Section 5 with someone.

Paper (PDF)

Back to Direct Style II: First-Class Continuations

Olivier Danvy and Julia L. Lawall. SIGPLAN Lisp Pointers V(1) (1992)

Paper (PDF)

A Lambda Calculus for Quantum Computation with Classical Control

Peter Selinger and Benoit Valiron. Mathematical. Structures in Comp. Sci. 16(3) (2006)

Paper (PDF)

Types and Type Inference in a Visual Programming Language

Margaret Burnett (1994)

Paper (PDF)

A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types

Chao-Hong Chen and Amr Sabry. Proc. ACM Program. Lang. 5(POPL) (2021)

Paper (PDF)

Intensional Datatype Refinement: With Application to Scalable Verification of Pattern-Match Safety

Eddie Jones and Steven Ramsay. Proc. ACM Program. Lang. 5(POPL) (2021)

Paper (PDF)

Probabilistic Numerics and Uncertainty in Computations

Philipp Hennig, Michael Osborne and Mark Girolami. Proceedings of the Royal Society A: Mathematical, Physical and Engineering Science 471 (2015)

Paper (PDF)

A Unified View of Modalities in Type Systems

Andreas Abel and Jean-Philippe Bernardy. Proc. ACM Program. Lang. 4(ICFP) (2020)

Skip Sections 6 to 8

Paper (PDF)

Is game semantics necessary?

Andreas Blass. Computer Science Logic: 66—77 (1994)

Paper (PDF)

Zippy LL(1) Parsing with Derivatives

Romain Edelmann, Jad Hamza and Viktor Kunčak. Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (2020)

Paper (PDF)

An Introduction to Algebraic Effects and Handlers. Invited Tutorial Paper

Matija Pretnar. Electron. Notes Theor. Comput. Sci. 319(C) (2015)

Paper (PDF)

A Typed Foundation for Directional Logic Programming

Uday S. Reddy. Proceedings of the Third International Workshop on Extensions of Logic Programming (1992)

Paper (PDF)

Incorrectness Logic

Peter W. O’Hearn. Proc. ACM Program. Lang. 4(POPL) (2019)

Paper (PDF)

Idris 2: Quantitative Type Theory in Action

Edwin Brady (2020)

Paper (PDF)

Aspect-Oriented Programming and Modular Reasoning

Gregor Kiczales and Mira Mezini. Proceedings of the 27th International Conference on Software Engineering (2005)

Paper (PDF)

Revisiting Information Hiding: Reflections on Classical and Nonclassical Modularity

Klaus Ostermann, Paolo G. Giarrusso, Christian Kästner and Tillmann Rendel. ECOOP 2011 -- Object-Oriented Programming: 155—178 (2011)

Paper (PDF)

Monoids: Theme and Variations (Functional Pearl)

Brent A. Yorgey. SIGPLAN Not. 47(12) (2012)

Paper (PDF)

One VM to Rule Them All

Thomas Würthinger, Christian Wimmer, Andreas Wöß, Lukas Stadler, Gilles Duboscq, Christian Humer, Gregor Richards, Doug Simon and Mario Wolczko. Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software (2013)

Paper (PDF)

Syntax and Semantics of Quantitative Type Theory

Robert Atkey. Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (2018)

We will not discuss Section 3.

Paper (PDF)

Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types

Andrea Vezzosi, Anders Mörtberg and Andreas Abel. Proc. ACM Program. Lang. 3(ICFP) (2019)

We only discuss pages 1 - 13.

Paper (PDF)

Polymorphic typed defunctionalization and concretization

François Pottier and Nadji Gauthier. Higher-Order and Symbolic Computation 19(1): 125—162 (2006)

We only discuss up to and including Section 6.

Paper (PDF)

Symmetry and Interactivity in Programming

P.-L. Curien. Bulletin of Symbolic Logic 9(2) (2003)

Paper (PDF)

Abstracting Definitional Interpreters (Functional Pearl)

David Darais, Nicholas Labich, Phúc C. Nguyen and David Van Horn. Proc. ACM Program. Lang. 1(ICFP) (2017)

Paper (PDF)

Dependent Object Types with Implicit Functions

Alex Jeffery. Proceedings of the Tenth ACM SIGPLAN Symposium on Scala: 1—11 (2019)

Paper (PDF)

Eta-expansion Does The Trick

Olivier Danvy, Karoline Malmkjær and Jens Palsberg. ACM Trans. Program. Lang. Syst. 18(6): 730—751 (1996)

Paper (PDF)

Declarative Programming

Sebastian Fischer (2009)

Please start reading from section 1.2 on page 15.

Paper (PDF)

Coeffects: A Calculus of Context-dependent Computation

Tomas Petricek, Dominic Orchard and Alan Mycroft. Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming: 123—135 (2014)

We will not discuss section 5.

Paper (PDF)

Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing

Paul Downen and Zena M. Ariola. 27th EACSL Annual Conference on Computer Science Logic (CSL 2018) (2018)

Paper (PDF)

Codata in Action

Paul Downen, Zachary Sullivan, Zena M. Ariola and Simon Peyton Jones. Proc. of ESOP: 119—146 (2019)

Paper (PDF)

Focusing and Higher-order Abstract Syntax

Noam Zeilberger. Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages: 359—369 (2008)

Paper (PDF)

When and How to Develop Domain-specific Languages

Marjan Mernik, Jan Heering and Anthony M. Sloane. ACM Comput. Surv. 37(4): 316—344 (2005)

Paper (PDF)

Extensible Denotational Language Specifications

Robert Cartwright and Matthias Felleisen. Proceedings of the International Conference on Theoretical Aspects of Computer Software: 244—272 (1994)

Paper (PDF)

Making Money Using Math

Erik Meijer. Queue 15(1) (2017)

Paper (PDF)

Proofs for Free: Parametricity for Dependent Types

Jean-philippe Bernardy, Patrik Jansson and Ross Paterson. J. Funct. Program. 22(2) (2012)

We will discuss sections 5, 6 and 7.

Paper (PDF)

Proofs for Free: Parametricity for Dependent Types

Jean-philippe Bernardy, Patrik Jansson and Ross Paterson. J. Funct. Program. 22(2) (2012)

We will only discuss sections 1, 2 and 3.

Paper (PDF)

On Self-Interpterters for System T and other typed λ-Calculi

Andrej Bauer (2016)

Paper (PDF)

A Walk in the Semantic Park

Olivier Danvy, Jacob Johannsen and Ian Zerny. Proceedings of the 20th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation: 1—12 (2011)

Paper (PDF)

Handling Delimited Continuations with Dependent Types

Youyou Cong and Kenichi Asai. Proc. ACM Program. Lang. 2(ICFP) (2018)

We'll only discuss sections 1-4 and 6.

Paper (PDF)

Strict and Lazy Semantics for Effects: Layering Monads and Comonads

Andrew K. Hirsch and Ross Tate. Proc. ACM Program. Lang. 2(ICFP) (2018)

Paper (PDF)

Generic Programming of All Kinds

Alejandro Serrano and Victor Cacciari Miraldo. Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell: 41—54 (2018)

Paper (PDF)

Levity Polymorphism

Richard A. Eisenberg and Simon Peyton Jones. Proc. of PLDI: 525—539 (2017)

Paper (PDF)

Programming Language Foundations in Agda

Philip Wadler. Proc. of SMBF (2018)

Paper (PDF)

How Are Programs Found? Speculating About Language Ergonomics with Curry-Howard

Johannes Emerich. Proceedings of the 2016 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software: 212—223 (2016)

Paper (PDF)

Compiling with Continuations, Continued

Andrew Kennedy. Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming: 177—190 (2007)

Paper (PDF)

A Syntactic Approach to Type Soundness

A.K. Wright and M. Felleisen. Inf. Comput. 115(1): 38—94 (1994)

Paper (PDF)

Everybody's Got To Be Somewhere

Conor McBride. Electronic Proceedings in Theoretical Computer Science: 53—69 (2018)

Paper (PDF)

Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory (Extended Version)

Anton Setzer and Peter Hancock. Dependently Typed Programming (2005)

Paper (PDF)

Passing a Language Through the Eye of a Needle

Roberto Ierusalimschy, Luiz Henrique De Figueiredo and Waldemar Celes. Commun. ACM 54(7): 38—43 (2011)

Paper (PDF)

On the expressive power of programming languages

Matthias Felleisen. Science of Computer Programming 17(1) (1991)

Paper (PDF)

Just Do It: Simple Monadic Equational Reasoning

Jeremy Gibbons and Ralf Hinze. Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming: 2—14 (2011)

Paper (PDF)

Separation Logic: A Logic for Shared Mutable Data Structures

John C. Reynolds. Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science: 55—74 (2002)

We will only discuss sections 1 - 7.

Paper (PDF)

First-Class Type Classes

Matthieu Sozeau and Nicolas Oury. Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics: 278—293 (2008)

Paper (PDF)

In Search of Types

Stephen Kell. Proc. of Onward!: 227—241 (2014)

Paper (PDF)

On the unity of duality

Noam Zeilberger. Annals of Pure and Applied Logic 153(1) (2008)

The focus will be on sections 2 and 3. We will not discuss the proofs in detail.

Paper (PDF)

A Monadic Framework for Delimited Continuations

R. Kent Dyvbig, Simon Peyton Jones and Amr Sabry. J. Funct. Program. 17(6): 687—730 (2007)

We will not read section 5 and only gloss over sections 6 and 7.

Paper (PDF)

An evaluation semantics for classical proofs

C. R. Murthy. Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science: 96—107 (1991)

Paper (PDF)

Unifying Structured Recursion Schemes

Ralf Hinze, Nicolas Wu and Jeremy Gibbons. Proc. of ICFP: 209—220 (2013)

Paper (PDF)

Eliminating Dependent Pattern Matching

Healfdene Goguen, Conor McBride and James McKinna. Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday: 521—540 (2006)

Paper (PDF)

Wellfounded Recursion with Copatterns: A Unified Approach to Termination and Productivity

Andreas M. Abel and Brigitte Pientka. Proc. of ICFP: 185—196 (2013)

Paper (PDF)

Programming with ornaments

Hsiang-Shang Ko and Jeremy Gibbons. Journal of Functional Programming 27 (2016)

Paper (PDF)

Representing Control: a Study of the CPS Transformation

Oliver Danvy and Andrzex Filinski. Mathematical Structures in Computer Science 2(4) (1992)

Paper (PDF)

The Duality of Construction

Paul Downen and Zena M. Ariola. Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410: 249—269 (2014)

Paper (PDF)

Classes and Mixins

Matthew Flatt, Shriram Krishnamurthi and Matthias Felleisen. Proc. of POPL: 171—183 (1998)

Paper (PDF)

Introducing a Calculus of Effects and Handlers for Natural Language Semantics

Jirka Maršík and Maxime Amblard. Formal Grammar : 20th and 21st International Conferences, FG 2015, Barcelona, Spain, August 2015, Revised Selected Papers. FG 2016, Bozen, Italy, August 2016, Proceedings: 257—272 (2016)

Paper (PDF)

Feature-Oriented Programming with Object Algebras

Bruno C. d. S. Oliveira, Tijs van der Storm, Alex Loh and William R. Cook. Proc. of ECOOP: 27—51 (2013)

Paper (PDF)

Shift to control

Chung-chieh Shan. Proc. of Scheme Workshop: 99—107 (2004)

Paper (PDF)

Generalizing Inference Systems by Coaxioms

Davide Ancona, Francesco Dagnino and Elena Zucca. Proc. of ESOP: 29—55 (2017)

Paper (PDF)

Objects and Classes, Co-algebraically

Bart Jacobs. Object Orientation with Parallelism and Persistence: 83—103 (1996)

Paper (PDF)

The expression lemma

Ralf Lämmel and Ondrej Rypacek. Proc. of MPC (2008)

Paper (PDF)

Halide: A Language and Compiler for Optimizing Parallelism, Locality, and Recomputation in Image Processing Pipelines

Jonathan Ragan-Kelley, Connelly Barnes, Andrew Adams, Sylvain Paris, Frédo Durand and Saman Amarasinghe. Proc. of PLDI: 519—530 (2013)

Paper (PDF)

Do Be Do Be Do

Sam Lindley, Conor McBride and Craig McLaughlin. Proc. of POPL: 500—514 (2017)

Paper (PDF)

Staging Generic Programming

Jeremy Yallop. Proc. of PEPM: 85—96 (2016)

Paper (PDF)

Farms, Pipes, Streams and Reforestation: Reasoning About Structured Parallel Processes Using Types and Hylomorphisms

David Castro, Kevin Hammond and Susmit Sarkar. Proc. of ICFP: 4—17 (2016)

Paper (PDF)

Focusing on Pattern Matching

Neelakantan R. Krishnaswami. Proc. of POPL: 366—378 (2009)

Paper (PDF)

Beta Reduction is Invariant, Indeed

Beniamino Accattoli and Ugo Dal Lago. Proc. of CSL-LICS (2014)

Paper (PDF)

Generating Performance Portable Code Using Rewrite Rules: From High-level Functional Expressions to High-performance OpenCL Code

Michel Steuwer, Christian Fensch, Sam Lindley and Christophe Dubach. Proc. of ICFP: 205—217 (2015)

Paper (PDF)

Stream Fusion, to Completenes

Smaragdakis Kiselyov, Biboudis, Palladinos. Proc. of POPL (2017)

Paper (PDF)

seL4: Formal Verification of an OS Kernel

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood. Proc. of SOSP: 207—220 (2009)

Paper (PDF)

DART: Directed Automated Random Testing

Patrice Godefroid, Nils Klarlund and Koushik Sen. Proc. of PLDI: 213—223 (2005)

Paper (PDF)

Difficulties in Learning Inheritance and Polymorphism

Neomi Liberman, Catriel Beeri and Yifat Ben-David Kolikant. ACM TOCE (Transactions on Computing Education) 11(1) (2011)

Paper (PDF)

Oh Lord, Please Don't Let Contracts Be Misunderstood (Functional Pearl)

Christos Dimoulas, Max S. New, Robert Bruce Findler and Matthias Felleisen. Proc. of ICFP: 117—131 (2016)

Paper (PDF)

A Virtual Class Calculus (Extended Version)

Erik Ernst, Klaus Ostermann and William R. Cook. Proc. of POPL: 270—282 (2006)

Paper (PDF)

The Constrained-monad Problem

Neil Sculthorpe, Jan Bracker, George Giorgidze and Andy Gill. Proc. of ICFP: 287—298 (2013)

Paper (PDF)

Does Homotopy Type Theory Provide a Foundation for Mathematics?

James Ladyman and Stuart Presnell. The British Journal for the Philosophy of Science (2016)

Paper (PDF)

The Essence of Multi-stage Evaluation in LMS

Tiark Rompf. In: A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday: 318—335 (2016)

Paper (PDF)

Can Programming Be Liberated from the Von Neumann Style? A Functional Style and Its Algebra of Programs

John Backus. Commun. ACM 21(8): 613—641 (1978)

Paper (PDF)

Mini-languages: a way to learn programming principles

Peter Brusilovsky, Eduardo Calabrese, Jozef Hvorecky, Anatoly Kouchnirenko and Philip Miller. Education and Information Technologies 2(1): 65—83 (1997)

Paper (PDF)

Complete and Decidable Type Inference for GADTs

Tom Schrijvers, Simon Peyton Jones, Martin Sulzmann and Dimitrios Vytiniotis. Proc. of ICFP: 341—352 (2009)

This link has a version later than the proceedings, so please use this.

Paper (PDF)

Types As Intervals

Robert Cartwright. Proc. of POPL: 22—36 (1985)

Paper (PDF)

Arrows, Robots, and Functional Reactive Programming

Paul Hudak, Antony Courtney, Henrik Nilsson and John Peterson. In: Advanced Functional Programming (AFP): 4th International School, 2002. Revised Lectures: 159—187 (2003)

Paper (PDF)

The Essence of Dependent Object Types

Nada Amin, Karl Samuel Grütter, Martin Odersky, Tiark Rompf and Sandro Stucki. Proc. of WadlerFest (2016)

Paper (PDF)

Everything Old is New Again: Quoted Domain-specific Languages

Shayan Najd, Sam Lindley, Josef Svenningsson and Philip Wadler. Proc. of PEPM: 25—36 (2016)

Paper (PDF)

The Design and Implementation of a Verification Technique for GPU Kernels

Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson and John Wickerson. ACM Trans. Program. Lang. Syst. 37(3) (2015)

We'll discuss Sec. 2+3 only (14 pages).

Paper (PDF)

Evaluation of Games for Teaching Computer Science

Ben Gibson and Tim Bell. Proc. of 8th Workshop in Primary and Secondary Computing Education: 51—60 (2013)

Paper (PDF)

Lightweight implementations of probabilistic programming languages via transformational compilation

David Wingate, Andreas Stuhlmueller and Noah D. Goodman. International Conference on Artificial Intelligence and Statistics: 770—778 (2011)

Paper (PDF)

Guarded Recursive Datatype Constructors

Hongwei Xi, Chiyan Chen and Gang Chen. Proc. of POPL: 224—235 (2003)

Paper (PDF)

Modularity and Implementation of Mathematical Operational Semantics

Mauro Jaskelioff, Neil Ghani and Graham Hutton. Proc. of Mathematically Structured Functional Programming (2008)

Paper (PDF)

Freer Monads, More Extensible Effects

Oleg Kiselyov and Hiromi Ishii. Proc. of Haskell Symposium: 94—105 (2015)

Paper (PDF)

Managing the development of large software systems: Concepts and techniques

W. W. Royce. Technical Papers of Western Electronic Show and Convention (WesCon) (1970)

This paper introduced the waterfall model of software development.

Paper (PDF)

Copy and Paste Redeemed

Krishna Narasimhan and Christoph Reichenbach. Proc. of ASE (2015)

Paper (PDF)

Stochastic Lambda Calculus and Monads of Probability Distributions

Norman Ramsey and Avi Pfeffer. Proc. of POPL: 154—165 (2002)

Paper (PDF)

Polymorphic Typed Defunctionalization

François Pottier and Nadji Gauthier. Proc. of POPL: 89—98 (2004)

Paper (PDF)

Functional Programming with Structured Graphs

Bruno C.d.S. Oliveira and William R. Cook. Proc. of ICFP: 77—88 (2012)

Paper (PDF)

F-ing Modules

Andreas Rossberg, Claudio V. Russo and Derek Dreyer. Proc. of TLDI: 89—102 (2010)

Paper (PDF)

Monad Transformers and Modular Interpreters

Sheng Liang, Paul Hudak and Mark Jones. Proc. of POPL: 333—343 (1995)

Paper (PDF)

A dissection of L

Arnaud Spiwack (2014)

We will skip Sec. 5.

Paper (PDF)

Resource-Safe Systems Programming with Embedded Domain Specific Languages

Edwin Brady and Kevin Hammond. Proc. of PADL: 242—257 (2012)

Paper (PDF)

Semantics of context-free languages

Donald E. Knuth. Mathematical systems theory 2(2): 127—145 (1968)

Paper (PDF)

Monads for Functional Programming

Philip Wadler. Advanced Functional Programming, Spring School: 24—52 (1995)

Paper (PDF)

Cross-Language Code Analysis and Refactoring

P. Mayer and A. Schroeder. Proc. of Source Code Analysis and Manipulation (SCAM): 94—103 (2012)

Paper (PDF)

Selective Memoization

Umut A. Acar, Guy E. Blelloch and Robert Harper. Proc. of POPL: 14—25 (2003)

Paper (PDF)

Packrat Parsers Can Support Left Recursion

Alessandro Warth, James R. Douglass and Todd Millstein. Proc. of PEPM: 103—110 (2008)

Paper (PDF)

Combinators for Bi-directional Tree Transformations: A Linguistic Approach to the View Update Problem

J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce and Alan Schmitt. Proc. of POPL: 233—246 (2005)

Paper (PDF)

To CNF or not to CNF? An efficient yet presentable version of the CYK algorithm

Martin Lange and Hans Leiß. Informatica Didactica 8: 2008—2010 (2009)

Paper (PDF)

Embedded Probabilistic Programming

Oleg Kiselyov and Chung-Chieh Shan. IFIP TC 2 Working Conference on Domain-Specific Languages: 360—384 (2009)

Additional resources available at http://okmij.org/ftp/kakuritu/.

Paper (PDF)

An Empirical Study of Regression Testing Techniques Incorporating Context and Lifetime Factors and Improved Cost-benefit Models

Hyunsook Do and Gregg Rothermel. 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering: 141—151 (2006)

Paper (PDF)

Towards a theory of type structure

John C. Reynolds. Programming Symposium: 408—425 (1974)

This is the paper that introduced System F.

Paper (PDF)

A Generic Account of Continuation-passing Styles

John Hatcliff and Olivier Danvy. Proc. of POPL: 458—471 (1994)

Paper (PDF)

A Denotational Semantics of Inheritance and Its Correctness

W. Cook and J. Palsberg. Proc. of OOPSLA: 433—443 (1989)

Paper (PDF)

Pattern matching without K

Jesper Cockx, Dominique Devriese and Frank Piessens. Proc. of ICFP: 257—268 (2014)

You should jump over Sec. 3 (the correctness proof) if you get stuck.

Paper (PDF)

Polytypic values possess polykinded types

Ralf Hinze. Mathematics of Program Construction: 2—27 (2000)

We will read sections 1–5. Timeslot: 16:00-17:00.

Paper (PDF)

Subject-oriented Programming: A Critique of Pure Objects

William Harrison and Harold Ossher. Proc. of OOPSLA: 411—428 (1993)

We will only discuss sections 1-6. Timeslot: 15:00-16:00.

Paper (PDF)

Points-to Analysis in Almost Linear Time

Bjarne Steensgaard. Proc. of POPL: 32—41 (1996)

Paper (PDF)

Codatatypes in ML

Tatsuya Hagino. Journal of Symbolic Computation 8(6): 629—650 (1989)

Paper (PDF)

Comparing object encodings

Kim B. Bruce, Luca Cardelli and Benjamin C. Pierce. Theoretical Aspects of Computer Software: 415—438 (1997)

Paper (PDF)

On the criteria to be used in decomposing systems into modules

David L. Parnas. Commun. ACM 15(12): 1053—1058 (1972)

Paper (PDF)

The Essence of the Iterator Pattern

Jeremy Gibbons and Bruno C. d. S. Oliveira. J. Funct. Program. 19(3-4): 377—402 (2009)

Paper (PDF)

Local Reasoning about Programs that Alter Data Structures

Peter O'Hearn, John Reynolds and Hongseok Yang. Workshop on Computer Science Logic: 1—19 (2001)

This is the paper that introduced separation logic, a very influential and useful variant of Hoare logic.

Paper (PDF)

An axiomatic basis for computer programming

C. A. R. Hoare. Commun. ACM 12(10): 576—580 (1969)

This is the paper that introduced Hoare logic.

Paper (PDF)