CS7470 Seminar in PL: Influential Ideas in Programming Languages (Spring 2026)
Some suggested starting points on influential ideas
Abstracting Abstract Machines
David Van Horn, Matthew Might.
In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010), Baltimore, Maryland, USA, 2010. PDF
From System F to Typed Assembly Language
Greg Morrisett, David Walker, Karl Crary, Neal Glew. ACM Transactions on Programming Languages and Systems (TOPLAS), 21(3):528-569, 1999. PDF
Proof-Carrying Code
George C. Necula.
In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1997), Paris, France, ACM, 1997. PDF
The CompCert Verified Compiler (project representative citation)
Xavier Leroy.
Formal Verification of a Realistic Compiler. Communications of the ACM, 52(7):107-115, 2009.
CompCert website (papers and PDFs)
BI as an Assertion Language for Mutable Data Structures
Samin Ishtiaq, Peter W. O’Hearn.
In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2001), London, UK, ACM, 2001. PDF
Simple Relational Correctness Proofs for Static Analyses and Program Transformations
Nick Benton.
In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), Venice, Italy, ACM, 2004. PDF (via ACM DL)
Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, Derek Dreyer.
In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2015), Mumbai, India, ACM, 2015.
Iris project (papers and PDFs)
1ML -- Core and Modules United
Andreas Rossberg.
In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), Vancouver, Canada, ACM, 2015. PDF
Refinement Types for Haskell
Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, Simon Peyton Jones.
In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP 2014), Gothenburg, Sweden, ACM, 2014. PDF
Handlers in Action
Ohad Kammar, Sam Lindley, Nicolas Oury.
In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP 2013), Boston, Massachusetts, USA, ACM, 2013. PDF
Frenetic: A Network Programming Language
Nate Foster, Rob Harrison, Michael J. Freedman, Christopher Monsanto, Jennifer Rexford, Alec Story, David Walker.
In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), Tokyo, Japan, ACM, 2011. PDF
CCured: Types for Safe C
George C. Necula, Scott McPeak, Shree P. Rahul, Westley Weimer.
In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), Berlin, Germany, ACM, 2002. PDF
Checked C: Making C Safe by Extension
Manuel Fähndrich, Santosh Nagarakatte, David Tarditi, et al.
Representative paper in Proceedings of the 2019 IEEE Security and Privacy Workshops (SPW), IEEE, 2019. PDF
QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs
Koen Claessen, John Hughes.
In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP 2000), Montreal, Canada, ACM, 2000. PDF
Gradual Typing for Functional Languages
Jeremy G. Siek, Walid Taha.
In Schemer Workshop, 2006. A foundational paper introducing gradual typing for functional languages. [web:31] PDF
Contracts for Higher-Order Functions
Robert Bruce Findler, Matthias Felleisen.
In Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming (ICFP 2002), Pittsburgh, USA, pp. 48–59, ACM, 2002. [web:31] PDF
Operational Semantics for Multi-Language Programs
Jacob Matthews and Robert Bruce Findler.
In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), Nice, France, ACM, 2007. PDF
Semantic Soundness for Language Interoperability
In Proceedings of the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2022), ACM, 2022. PDF (example link)
Halide: A Language and Compiler for Optimizing Parallelism, Locality, and Recomputation in Image Processing Pipelines
Jonathan Ragan-Kelley, Andrew Adams, Sylvain Paris, Marc Levoy, Saman Amarasinghe, Fredo Durand, et al.
In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2013), Seattle, Washington, USA, ACM, 2013. PDF
Proving Differential Privacy via Probabilistic Couplings
Gilles Barthe, Boris Kopf, Federico Olmedo, Santiago Zanella Beguelin, Justin Hsu (author lists vary slightly by version).
In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016), New York, NY, USA, IEEE, 2016. PDF
KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs
Cristian Cadar, Daniel Dunbar, Dawson Engler.
In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008), San Diego, CA, USA, USENIX, 2008. PDF
A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages
Reference? PDF
Software Model Checking
Ranjit Jhala, Rupak Majumdar.
Survey-style paper on software model checking, ACM Computing Surveys, 41(4):21:1-21:54, 2009. PDF
Automatic Predicate Abstraction of C Programs
Thomas Ball, Rupak Majumdar, Todd Millstein, Sriram K. Rajamani.
In Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation (PLDI 2001), Snowbird, Utah, USA, ACM, 2001. PDF
Counterexample-Guided Abstraction Refinement
Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith.
In Proceedings of the 12th International Conference on Computer Aided Verification (CAV 2000), LNCS 1855, Springer, 2000. PDF
Amal Ahmed
Last modified: Wed Jan 7 14:17:42 EST 2026