2015

• Michael Greenberg,Space-Efficient Manifest Contracts.
• Hamid Ebadi,David Sands,Gerardo Schneider,Differential Privacy: Now it's Getting Personal.
• Karl Crary,Michael J. Sullivan,A Calculus for Relaxed Memory.
• Adam Chlipala,Ur/Web: A Simple Model for Programming the Web.
• Damien Pous,Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests.
• Gordon Stewart,Lennart Beringer,Santiago Cuellar,Andrew W. Appel,Compositional CompCert.
• Osbert Bastani,Saswat Anand,Alex Aiken,Specification Inference Using Context-Free Language Reachability.
• Ahmed Bouajjani,Michael Emmi,Constantin Enea,Jad Hamza,Tractable Refinement Checking for Concurrent Objects.
• Luísa Lourenço,Luís Caires,Dependent Information Flow Types.
• Gilles Barthe,Marco Gaboardi,Emilio Jesús Gallego Arias,Justin Hsu,Aaron Roth,Pierre-Yves Strub,Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy.
• Jacques-Henri Jourdan,Vincent Laporte,Sandrine Blazy,Xavier Leroy,David Pichardie,A Formally-Verified C Static Analyzer.
• Robert A. Cochran,Loris D'Antoni,Benjamin Livshits,David Molnar,Margus Veanes,Program Boosting: Program Synthesis via Crowd-Sourcing.
• Sam Staton,Algebraic Effects, Linearity, and Quantum Programming Languages.
• Krishnendu Chatterjee,Andreas Pavlogiannis,Yaron Velner,Quantitative Interprocedural Analysis.
• Fei He,Xiaowei Gao,Bow-Yaw Wang,Lijun Zhang,Leveraging Weighted Automata in Compositional Reasoning about Concurrent Probabilistic Systems.
• Venmugil Elango,Fabrice Rastello,Louis-Noël Pouchet,J. Ramanujam,P. Sadayappan,On Characterizing the Data Access Complexity of Programs.
• Oded Padon,Neil Immerman,Aleksandr Karbyshev,Ori Lahav,Mooly Sagiv,Sharon Shoham,Decentralizing SDN Policies.
• Adam Chlipala,From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification.
• Kristina Sojakova,Higher Inductive Types as Homotopy-Initial Algebras.
• Julien Lange,Emilio Tuosto,Nobuko Yoshida,From Communicating Machines to Graphical Choreographies.
• Ronghui Gu,Jérémie Koenig,Tahina Ramananandro,Zhong Shao,Xiongnan (Newman) Wu,Shu-Chun Weng,Haozhong Zhang,Yu Guo,Deep Specifications and Certified Abstraction Layers.
• Azadeh Farzan,Zachary Kincaid,Andreas Podelski,Proof Spaces for Unbounded Parallelism.
• Neelakantan R. Krishnaswami,Pierre Pradic,Nick Benton,Integrating Linear and Dependent Types.
• Luis María Ferrer Fioriti,Holger Hermanns,Probabilistic Termination: Soundness, Completeness, and Compositionality.
• Kazunori Tobisawa,A Meta Lambda Calculus with Cross-Level Computation.
• Veselin Raychev,Martin T. Vechev,Andreas Krause,Predicting Program Properties from "Big Code".
• Hao Tang,Xiaoyin Wang,Lingming Zhang,Bing Xie,Lu Zhang,Hong Mei,Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks.
• Ashutosh Gupta,Thomas A. Henzinger,Arjun Radhakrishna,Roopsha Samanta,Thorsten Tarrach,Succinct Representation of Concurrent Trace Sets.
• Rajeev Alur,Loris D'Antoni,Mukund Raghothaman,DReX: A Declarative Language for Efficiently Evaluating Regular String Transformations.
• Ralf Jung,David Swasey,Filip Sieczkowski,Kasper Svendsen,Aaron Turon,Lars Birkedal,Derek Dreyer,Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning.
• Michael D. Adams,Towards the Essence of Hygiene.
• Davide Sangiorgi,Equations, Contractions, and Unique Solutions.
• Ralf Hinze,Nicolas Wu,Jeremy Gibbons,Conjugate Hylomorphisms - Or: The Mother of All Structured Recursion Schemes.
• Giuseppe Castagna,Kim Nguyen,Zhiwu Xu,Pietro Abate,Polymorphic Functions with Set-Theoretic Types: Part 2: Local Type Inference and Type Reconstruction.
• Benjamin Delaware,Clément Pit-Claudel,Jason Gross,Adam Chlipala,Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant.
• Vilhelm Sjöberg,Stephanie Weirich,Programming up to Congruence.
• Roberto Giacobazzi,Francesco Logozzo,Francesco Ranzato,Analyzing Program Analyses.
• Ronald Garcia,Matteo Cimini,Principal Type Schemes for Gradual Programs.
• Aseem Rastogi,Nikhil Swamy,Cédric Fournet,Gavin M. Bierman,Panagiotis Vekris,Safe & Efficient Gradual Typing for TypeScript.
• Denis Bogdanas,Grigore Rosu,K-Java: A Complete Semantics of Java.
• Pieter Agten,Bart Jacobs,Frank Piessens,Sound Modular Verification of C Code Executing in an Unverified Context.
• Minh Ngo,Fabio Massacci,Dimiter Milushev,Frank Piessens,Runtime Enforcement of Security Policies on Black Box Reactive Programs.
• Margus Veanes,Todd Mytkowicz,David Molnar,Benjamin Livshits,Data-Parallel String-Manipulating Programs.
• Krishnendu Chatterjee,Rasmus Ibsen-Jensen,Andreas Pavlogiannis,Prateesh Goyal,Faster Algorithms for Algebraic Path Properties in Recursive State Machines with Constant Treewidth.
• Taro Sekiyama,Yuki Nishida,Atsushi Igarashi,Manifest Contracts for Datatypes.
• Filippo Bonchi,Pawel Sobocinski,Fabio Zanasi,Full Abstraction for Signal Flow Graphs.
• Paul-André Melliès,Noam Zeilberger,Functors are Type Refinement Systems.
• Mike Dodds,Andreas Haas,Christoph M. Kirsch,A Scalable, Correct Time-Stamped Stack.
• Matt Brown,Jens Palsberg,Self-Representation in Girard's System U.
• Mila Dalla Preda,Roberto Giacobazzi,Arun Lakhotia,Isabella Mastroeni,Abstract Symbolic Automata: Mixed syntactic/semantic similarity analysis of executables.
• 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.
• Nate Foster,Dexter Kozen,Matthew Milano,Alexandra Silva,Laure Thompson,A Coalgebraic Decision Procedure for NetKAT.

2014

• Andrew Cave,Francisco Ferreira,Prakash Panangaden,Brigitte Pientka,Fair reactive programming.
• Stephen Chang,Matthias Felleisen,Profiling for laziness.
• Shachar Itzhaky,Anindya Banerjee,Neil Immerman,Ori Lahav,Aleksandar Nanevski,Mooly Sagiv,Modular reasoning about heap paths via effectively propositional formulas.
• Eva Darulova,Viktor Kuncak,Sound compilation of reals.
• Stefano Dissegna,Francesco Logozzo,Francesco Ranzato,Tracing compilation by abstract interpretation.
• James Brotherston,Jules Villard,Parametric completeness for separation theories.
• Vijay D'Silva,Leopold Haller,Daniel Kroening,Abstract satisfaction.
• Thomas Ehrhard,Christine Tasson,Michele Pagani,Probabilistic coherence spaces are fully abstract for probabilistic PCF.
• Shin-ya Katsumata,Parametric effect monads and semantics of effect systems.
• Patrick Cousot,Radhia Cousot,A Galois connection calculus for abstract interpretation.
• Robert Atkey,From parametricity to conservation laws, via Noether's theorem.
• Swarat Chaudhuri,Martin Clochard,Armando Solar-Lezama,Bridging boolean and quantitative synthesis using smoothed proof search.
• Andrzej S. Murawski,Nikos Tzevelekos,Game semantics for interface middleweight Java.
• Nathan Chong,Alastair F. Donaldson,Jeroen Ketema,A sound and complete abstraction for reasoning about parallel prefix sums.
• Devin Coughlin,Bor-Yuh Evan Chang,Fissile type analysis: modular checking of almost everywhere invariants.
• Andrew Miller,Michael Hicks,Jonathan Katz,Elaine Shi,Authenticated data structures, generically.
• Ilya Sergey,Dimitrios Vytiniotis,Simon L. Peyton Jones,Modular, higher-order cardinality analysis in theory and practice.
• Lindsey Kuper,Aaron Turon,Neelakantan R. Krishnaswami,Ryan R. Newton,Freeze after writing: quasi-deterministic parallel programming with LVars.
• Chris Casinghino,Vilhelm Sjöberg,Stephanie Weirich,Combining proofs and programs in a dependently typed language.
• Richard A. Eisenberg,Dimitrios Vytiniotis,Simon L. Peyton Jones,Stephanie Weirich,Closed type families with overlapping equations.
• Yi Li,Aws Albarghouthi,Zachary Kincaid,Arie Gurfinkel,Marsha Chechik,Symbolic optimization with SMT solvers.
• Sheng Chen,Martin Erwig,Counter-factual typing for debugging type errors.
• Beniamino Accattoli,Eduardo Bonelli,Delia Kesner,Carlos Lombardi,A nonstandard standardization theorem.
• Bertrand Jeannet,Peter Schrammel,Sriram Sankaranarayanan,Abstract acceleration of general linear loops.
• Ramana Kumar,Magnus O. Myreen,Michael Norrish,Scott Owens,CakeML: a verified implementation of ML.
• Lars Birkedal,Modular reasoning about concurrent higher-order imperative programs.
• Andrew D. Gordon,Thore Graepel,Nicolas Rolland,Claudio V. Russo,Johannes Borgström,John Guiver,Tabular: a schema-driven probabilistic programming language.
• Fan Long,Stelios Sidiroglou-Douskos,Deokhwan Kim,Martin C. Rinard,Sound input filter generation for integer overflow errors.
• Michele Pagani,Peter Selinger,Benoît Valiron,Applying quantitative semantics to higher-order quantum computing.
• Martin Bodin,Arthur Charguéraud,Daniele Filaretti,Philippa Gardner,Sergio Maffeis,Daiva Naudziuniene,Alan Schmitt,Gareth Smith,A trusted mechanised JavaSript specification.
• Swarat Chaudhuri,Azadeh Farzan,Zachary Kincaid,Consistency analysis of decision-making programs.
• Robbert Krebbers,An operational and axiomatic semantics for non-determinism and sequence points in C.
• Tewodros A. Beyene,Swarat Chaudhuri,Corneliu Popeea,Andrey Rybalchenko,A constraint-based approach to solving games on infinite graphs.
• Udi Boker,Thomas A. Henzinger,Arjun Radhakrishna,Battery transition systems.
• Azadeh Farzan,Zachary Kincaid,Andreas Podelski,Proofs that count.
• Nikhil Swamy,Cédric Fournet,Aseem Rastogi,Karthikeyan Bhargavan,Juan Chen,Pierre-Yves Strub,Gavin M. Bierman,Gradual typing embedded securely in JavaScript.
• Arthur Azevedo de Amorim,Nathan Collins,André DeHon,Delphine Demange,Catalin Hritcu,David Pichardie,Benjamin C. Pierce,Randy Pollack,Andrew Tolmach,A verified information-flow architecture.
• Parosh Aziz Abdulla,Stavros Aronis,Bengt Jonsson,Konstantinos F. Sagonas,Optimal dynamic partial order reduction.
• Gilles Barthe,Cédric Fournet,Benjamin Grégoire,Pierre-Yves Strub,Nikhil Swamy,Santiago Zanella Béguelin,Probabilistic relational verification for cryptographic implementations.
• Scott Kilpatrick,Derek Dreyer,Simon L. Peyton Jones,Simon Marlow,Backpack: retrofitting Haskell with interfaces.
• Nick Benton,Martin Hofmann,Vivek Nigam,Abstract effects and proof-relevant logical relations.
• Ugo Dal Lago,Davide Sangiorgi,Michele Alberti,On coinductive equivalences for higher-order probabilistic functional programs.
• Wonyeol Lee,Sungwoo Park,A proof system for separation logic with magic wand.
• Sebastian Burckhardt,Alexey Gotsman,Hongseok Yang,Marek Zawirski,Replicated data types: specification, verification, optimality.
• Gérard Huet,Hugo Herbelin,30 years of research and development around Coq.
• Zhe Hou,Ranald Clouston,Rajeev Goré,Alwen Tiu,Proof search for propositional abstract separation logics via labelled sequents.
• Carolyn Jane Anderson,Nate Foster,Arjun Guha,Jean-Baptiste Jeannin,Dexter Kozen,Cole Schlesinger,David Walker,NetkAT: semantic foundations for networks.
• Robert Atkey,Neil Ghani,Patricia Johann,A relationally parametric model of dependent type theory.
• Rahul Sharma,Aditya V. Nori,Alex Aiken,Bias-variance tradeoffs in program analysis.
• Danfeng Zhang,Andrew C. Myers,Toward general diagnosis of static errors.
• Giuseppe Castagna,Kim Nguyen,Zhiwu Xu,Hyeonseung Im,Sergueï Lenglet,Luca Padovani,Polymorphic functions with set-theoretic types: part 1: syntax, semantics, and evaluation.
• Steven J. Ramsay,Robin P. Neatherway,C.-H. Luke Ong,A type-directed abstraction refinement approach to higher-order model checking.
• Ahmed Bouajjani,Constantin Enea,Jad Hamza,Verifying eventual consistency of optimistic replication systems.
• Loris D'Antoni,Margus Veanes,Minimization of symbolic automata.
• Stephen Brookes,Peter W. O'Hearn,Uday S. Reddy,The essence of Reynolds.

2013

• Ugo Dal Lago,Barbara Petit,The geometry of types.
• Chung-Kil Hur,Georg Neis,Derek Dreyer,Viktor Vafeiadis,The power of parameterization in coinductive proof.
• Aquinas Hobor,Jules Villard,The ramifications of sharing in data structures.
• Guy E. Blelloch,Robert Harper,Cache and I/O efficent functional algorithms.
• Marco Gaboardi,Andreas Haeberlen,Justin Hsu,Arjun Narayan,Benjamin C. Pierce,Linear dependent types for differential privacy.
• Marco Carbone,Fabrizio Montesi,Deadlock-freedom-by-design: multiparty asynchronous global programming.
• Ruy Ley-Wild,Aleksandar Nanevski,Subjective auxiliary state for coarse-grained concurrency.
• Benjamin Livshits,Stephen Chong,Towards fully automatic placement of security sanitizers and declassifiers.
• Thomas Dinsdale-Young,Lars Birkedal,Philippa Gardner,Matthew J. Parkinson,Hongseok Yang,Views: compositional reasoning for concurrent programs.
• Kohei Suenaga,Hiroyoshi Sekine,Ichiro Hasuo,Hyperstream processing systems: nonstandard modeling of continuous-time signals.
• Jonas Braband Jensen,Nick Benton,Andrew Kennedy,High-level separation logic for low-level code.
• Ganesan Ramalingam,Kapil Vaswani,Fault tolerance via idempotence.
• Véronique Benzaken,Giuseppe Castagna,Kim Nguyen,Jérôme Siméon,Static and dynamic semantics of NoSQL languages.
• Hiroshi Unno,Tachio Terauchi,Naoki Kobayashi,Automating relatively complete verification of higher-order functional programs.
• Benjamin Delaware,Bruno C. d. S. Oliveira,Tom Schrijvers,Meta-theory à la carte.
• Tiark Rompf,Arvind K. Sujeeth,Nada Amin,Kevin J. Brown,Vojin Jovanovic,HyoukJoong Lee,Manohar Jonnalagedda,Kunle Olukotun,Martin Odersky,Optimizing data structures in high-level programs: new directions for extensible compilers based on staging.
• Filippo Bonchi,Damien Pous,Checking NFA equivalence with bisimulations up to congruence.
• Ross Tate,The sequential semantics of producer effect systems.
• Thomas A. Henzinger,Christoph M. Kirsch,Hannes Payer,Ali Sezgin,Ana Sokolova,Quantitative relaxation of concurrent data structures.
• Michael D. Adams,Principled parsing for indentation-sensitive languages: revisiting landin's offside rule.
• Mark Batty,Mike Dodds,Alexey Gotsman,Library abstraction for C/C++ concurrency.
• Richard Mayr,Lorenzo Clemente,Advanced automata minimization.
• Dimitrios Vytiniotis,Simon L. Peyton Jones,Koen Claessen,Dan Rosén,HALO: haskell to logic through denotational semantics.
• Pavol Cerný,Thomas A. Henzinger,Arjun Radhakrishna,Quantitative abstraction refinement.
• Sam Staton,Paul Blain Levy,Universal properties of impure programming languages.
• Robert Atkey,Patricia Johann,Andrew Kennedy,Abstraction and invariance for algebraically indexed types.
• Amir M. Ben-Amram,Samir Genaim,On the linear ranking problem for integer linear-constraint loops.
• Jonghyun Park,Jeongbong Seo,Sungwoo Park,A theorem prover for Boolean BI.
• Andrew D. Gordon,Mihhail Aizatulin,Johannes Borgström,Guillaume Claret,Thore Graepel,Aditya V. Nori,Sriram K. Rajamani,Claudio V. Russo,A model-learner pattern for bayesian reasoning.
• Ali Sinan Köksal,Yewen Pu,Saurabh Srivastava,Rastislav Bodík,Jasmin Fisher,Nir Piterman,Synthesis of biological models from mutation experiments.
• Andreas Abel,Brigitte Pientka,David Thibodeau,Anton Setzer,Copatterns: programming infinite structures by observations.
• Vijay D'Silva,Leopold Haller,Daniel Kroening,Abstract conflict driven learning.
• Luís Caires,João Costa Seco,The type discipline of behavioral separation.
• Cédric Fournet,Nikhil Swamy,Juan Chen,Pierre-Évariste Dagand,Pierre-Yves Strub,Benjamin Livshits,Fully abstract compilation to JavaScript.
• Ramakrishna Upadrasta,Albert Cohen,Sub-polyhedral scheduling using (unit-)two-variable-per-inequality polyhedra.
• Matko Botincan,Domagoj Babic,Sigma*: symbolic learning of input-output specifications.
• Delphine Demange,Vincent Laporte,Lei Zhao,Suresh Jagannathan,David Pichardie,Jan Vitek,Plan B: a buffered memory model for Java.
• Steffen Lösch,Andrew M. Pitts,Full abstraction for nominal Scott domains.
• Alexis Goyet,The Lambda Lambda-Bar calculus: a dual calculus for unconstrained strategies.
• Nishant Totla,Thomas Wies,Complete instantiation-based interpolation.
• Earl T. Barr,Thanh Vo,Vu Le,Zhendong Su,Automatic detection of floating-point exceptions.
• Aaron Joseph Turon,Jacob Thamsborg,Amal Ahmed,Lars Birkedal,Derek Dreyer,Logical relations for fine-grained concurrency.
• Azadeh Farzan,Zachary Kincaid,Andreas Podelski,Inductive data flow graphs.

2012

• Ali Sinan Köksal,Viktor Kuncak,Philippe Suter,Constraints as control.
• Sooraj Bhat,Ashish Agarwal,Richard W. Vuduc,Alexander G. Gray,A type theory for probability density functions.
• Aseem Rastogi,Avik Chaudhuri,Basil Hosmer,The ins and outs of gradual type inference.
• Daniel R. Licata,Robert Harper,Canonicity for 2-dimensional type theory.
• Casey Klein,John Clements,Christos Dimoulas,Carl Eastlund,Matthias Felleisen,Matthew Flatt,Jay A. McCarthy,Jon Rafkind,Sam Tobin-Hochstadt,Robert Bruce Findler,Run your research: on the effectiveness of lightweight mechanization.
• Uday S. Reddy,John C. Reynolds,Syntactic control of interference for separation logic.
• Mark Batty,Kayvan Memarian,Scott Owens,Susmit Sarkar,Peter Sewell,Clarifying and compiling C/C++ concurrency: from C++11 to POWER.
• Margus Veanes,Pieter Hooimeijer,Benjamin Livshits,David Molnar,Nikolaj Bjørner,Symbolic finite state transducers: algorithms and applications.
• Ohad Kammar,Gordon D. Plotkin,Algebraic foundations for effect-dependent optimisations.
• Azadeh Farzan,Zachary Kincaid,Verification of parameterized concurrent programs by modular reasoning about data and control.
• Chucky Ellison,Grigore Rosu,An executable formal semantics of C with applications.
• Ahmed Bouajjani,Michael Emmi,Analysis of recursively parallel programs.
• Donald Ray,Jay Ligatti,Defining code-injection attacks.
• Ravi Chugh,Patrick Maxim Rondon,Ranjit Jhala,Nested refinements: a logic for duck typing.
• Roshan P. James,Amr Sabry,Information effects.
• Julien Cretin,Didier Rémy,On the power of coercion abstraction.
• Mayur Naik,Hongseok Yang,Ghila Castelnuovo,Mooly Sagiv,Abstractions from tests.
• Phillip Heidegger,Annette Bieniusa,Peter Thiemann,Access permission contracts for scripting languages.
• Matko Botincan,Mike Dodds,Suresh Jagannathan,Resource-sensitive synchronization inference by abduction.
• Antonis Stampoulis,Zhong Shao,Static and user-extensible proof checking.
• Chung-Kil Hur,Derek Dreyer,Georg Neis,Viktor Vafeiadis,The marriage of bisimulations and Kripke logical relations.
• Stephan van Staden,Cristiano Calcagno,Bertrand Meyer,Freefinement.
• Samik Basu,Tevfik Bultan,Meriem Ouederni,Deciding choreography realizability.
• Zeyuan Allen Zhu,Sasa Misailovic,Jonathan A. Kelner,Martin C. Rinard,Randomized accuracy-aware program transformations for efficient approximate computations.
• Karl Naden,Robert Bocchino,Jonathan Aldrich,Kevin Bierhoff,A type system for borrowing permissions.
• Tony Hoare,Message of thanks: on the receipt of the 2011 ACM SIGPLAN distinguished achievement award.
• Thibaut Balabonski,A unified approach to fully lazy sharing.
• Neelakantan R. Krishnaswami,Nick Benton,Jan Hoffmann,Higher-order functional reactive programming in bounded space.
• Saurabh Joshi,Shuvendu K. Lahiri,Akash Lal,Underspecified harnesses and interleaved bugs.
• Tahina Ramananandro,Gabriel Dos Reis,Xavier Leroy,A mechanized semantics for C++ object construction and destruction, with applications to resource management.
• Jean Yang,Kuat Yessenov,Armando Solar-Lezama,A language for automatically enforcing privacy policies.
• Gilles Barthe,Boris Köpf,Federico Olmedo,Santiago Zanella Béguelin,Probabilistic relational reasoning for differential privacy.
• Thomas H. Austin,Cormac Flanagan,Multiple facets for dynamic information flow.
• Parthasarathy Madhusudan,Xiaokang Qiu,Andrei Stefanescu,Recursive proofs for inductive tree data-structures.
• Christopher Monsanto,Nate Foster,Rob Harrison,David Walker,A compiler and run-time system for network programming languages.
• Mikolaj Bojanczyk,Laurent Braud,Bartek Klin,Slawomir Lasota,Towards nominal computation.
• Martin Hofmann,Benjamin C. Pierce,Daniel Wagner,Edit lenses.
• Philippa Gardner,Sergio Maffeis,Gareth David Smith,Towards a program logic for JavaScript.
• Yannis Smaragdakis,Jacob Evans,Caitlin Sadowski,Jaeheon Yi,Cormac Flanagan,Sound predictive race detection in polynomial time.
• Andrew Cave,Brigitte Pientka,Programming with binders and indexed data-types.
• Patrick Cousot,Radhia Cousot,An abstract interpretation framework for termination.
• Jianzhou Zhao,Santosh Nagarakatte,Milo M. K. Martin,Steve Zdancewic,Formalizing the LLVM intermediate representation for verified program transformations.
• Krystof Hoder,Laura Kovács,Andrei Voronkov,Playing in the grey area of proofs.
• Pierre-Yves Strub,Nikhil Swamy,Cédric Fournet,Juan Chen,Self-certification: bootstrapping certified typecheckers in F* with Coq.
• Hongjin Liang,Xinyu Feng,Ming Fu,A rely-guarantee-based simulation for verifying concurrent program transformations.

2011

• Jesse A. Tov,Riccardo Pucella,Practical affine types.
• Amal Ahmed,Robert Bruce Findler,Jeremy G. Siek,Philip Wadler,Blame for all.
• Sumit Gulwani,Automating string processing in spreadsheets using input-output examples.
• Jaroslav Sevcík,Viktor Vafeiadis,Francesco Zappa Nardelli,Suresh Jagannathan,Peter Sewell,Relaxed-memory concurrency and verified compilation.
• Tarun Prabhu,Shreyas Ramalingam,Matthew Might,Mary W. Hall,EigenCFA: accelerating flow analysis with GPUs.
• Nikos Tzevelekos,Fresh-register automata.
• Byron Cook,Eric Koskinen,Making prophecies with decision predicates.
• Patrick Cousot,Radhia Cousot,Francesco Logozzo,A parametric segmentation functor for fully automatic and scalable array content analysis.
• Martin Hofmann,Benjamin C. Pierce,Daniel Wagner,Symmetric lenses.
• Chung-Kil Hur,Derek Dreyer,A kripke logical relation between ML and assembly.
• Isil Dillig,Thomas Dillig,Alex Aiken,Precise reasoning for programs using containers.
• P. Madhusudan,Gennaro Parlato,The tree width of auxiliary storage.
• Norman Ramsey,João Dias,Resourceable, retargetable, modular instruction selection using a machine-independent, type-based tiling of low-level intermediate code.
• Stephanie Weirich,Dimitrios Vytiniotis,Simon L. Peyton Jones,Steve Zdancewic,Generative type abstraction and type-level computation.
• François Pottier,A typed store-passing translation for general references.
• Yuan Feng,Runyao Duan,Mingsheng Ying,Bisimulation for quantum processes.
• Martin D. Schwarz,Helmut Seidl,Vesal Vojdani,Peter Lammich,Markus Müller-Olm,Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol.
• Mike Dodds,Suresh Jagannathan,Matthew J. Parkinson,Modular reasoning for deterministic parallelism.
• Pramod G. Joisha,Robert S. Schreiber,Prithviraj Banerjee,Hans-Juergen Boehm,Dhruva R. Chakrabarti,A technique for the effective and automatic reuse of classical compiler optimizations on multithreaded code.
• Dimitrios Prountzos,Roman Manevich,Keshav Pingali,Kathryn S. McKinley,A shape analysis for optimizing parallel graph programs.
• Bart Jacobs,Frank Piessens,Expressive modular fine-grained concurrency specification.
• Yannis Smaragdakis,Martin Bravenboer,Ondrej Lhoták,Pick your contexts well: understanding object-sensitivity.
• Jan Hoffmann,Klaus Aehlig,Martin Hofmann,Multivariate amortized resource analysis.
• Pierre-Malo Deniélou,Nobuko Yoshida,Dynamic multirole session types.
• Rajeev Alur,Pavol Cerný,Streaming transducers for algorithmic verification of single-pass list-processing programs.
• Ashutosh Gupta,Corneliu Popeea,Andrey Rybalchenko,Predicate abstraction and refinement for verifying multi-threaded programs.
• Fritz Henglein,Lasse Nielsen,Regular expression containment: coinductive axiomatization and computational interpretation.
• Percy Liang,Omer Tripp,Mayur Naik,Learning minimal abstractions.
• Lars Birkedal,Bernhard Reus,Jan Schwinghammer,Kristian Støvring,Jacob Thamsborg,Hongseok Yang,Step-indexed kripke models over recursive worlds.
• Anna Bendersky,Erez Petrank,Space overhead bounds for dynamic memory management with partial compaction.
• Javier Esparza,Pierre Ganty,Complexity of pattern-based verification for multithreaded programs.
• Xavier Rival,Bor-Yuh Evan Chang,Calling context abstraction with shapes.
• C.-H. Luke Ong,Steven J. Ramsay,Verifying higher-order functional programs with pattern-matching algebraic data types.
• Wontae Choi,Baris Aktemur,Kwangkeun Yi,Makoto Tatsuta,Static analysis of multi-staged programs via unstaging translation.
• Jong-hoon (David) An,Avik Chaudhuri,Jeffrey S. Foster,Michael Hicks,Dynamic inference of static types for ruby.
• Jérôme Leroux,Vector addition system reachability problem: a short self-contained proof.
• Louis-Noël Pouchet,Uday Bondhugula,Cédric Bastoul,Albert Cohen,J. Ramanujam,P. Sadayappan,Nicolas Vasilache,Loop transformations: convexity, pruning and optimization.
• Aaron Joseph Turon,Mitchell Wand,A separation logic for refining concurrent objects.
• Ondrej Lhoták,Kwok-Chiang Andrew Chung,Points-to analysis with efficient strong updates.
• Nishant Sinha,Chao Wang,On interference abstractions.
• Mark Batty,Scott Owens,Susmit Sarkar,Peter Sewell,Tjark Weber,Mathematizing C++ concurrency.
• Michael Emmi,Shaz Qadeer,Zvonimir Rakamaric,Delay-bounded scheduling.
• Tahina Ramananandro,Gabriel Dos Reis,Xavier Leroy,Formal verification of object layout for c++ multiple inheritance.
• Shu-yu Guo,Jens Palsberg,The essence of compiling with traces.
• Dan R. Ghica,Alex I. Smith,Geometry of synthesis III: resource management through type inference.
• Christos Dimoulas,Robert Bruce Findler,Cormac Flanagan,Matthias Felleisen,Correct blame for contracts: no more scapegoating.
• Robert L. Bocchino Jr.,Stephen Heumann,Nima Honarmand,Sarita V. Adve,Vikram S. Adve,Adam Welc,Tatiana Shpeisman,Safe nondeterminism in a deterministic-by-default parallel language.
• Matthew MacLaurin,The design of kodu: a tiny visual programming language for children on the Xbox 360.
• P. Madhusudan,Gennaro Parlato,Xiaokang Qiu,Decidable logics combining heap structures and data.
• Hagit Attiya,Rachid Guerraoui,Danny Hendler,Petr Kuznetsov,Maged M. Michael,Martin T. Vechev,Laws of order: expensive synchronization in concurrent algorithms cannot be eliminated.

2010

• Jean-Baptiste Tristan,Xavier Leroy,A simple, verified validator for software pipelining.
• Derek Dreyer,Georg Neis,Andreas Rossberg,Lars Birkedal,A relational modal logic for higher-order stateful ADTs.
• Jean-Phillipe Martin,Michael Hicks,Manuel Costa,Periklis Akritidis,Miguel Castro,Dynamically checking ownership policies in concurrent c/c++ programs.
• Limin Jia,Jianzhou Zhao,Vilhelm Sjöberg,Stephanie Weirich,Dependent types and program equivalence.
• Ross Tate,Michael Stepp,Sorin Lerner,Generating compiler optimizations from proofs.
• Rastislav Bodík,Satish Chandra,Joel Galenson,Doug Kimelman,Nicholas Tung,Shaon Barman,Casey Rodarmor,Programming with angelic nondeterminism.
• Aleksandar Nanevski,Viktor Vafeiadis,Josh Berdine,Structuring the verification of heap-manipulating programs.
• Saurabh Srivastava,Sumit Gulwani,Jeffrey S. Foster,From program verification to program synthesis.
• Patrice Godefroid,Aditya V. Nori,Sriram K. Rajamani,SaiDeep Tetali,Compositional may-must program analysis: unleashing the power of alternation.
• William R. Harris,Sriram Sankaranarayanan,Franjo Ivancic,Aarti Gupta,Program analysis via satisfiability modulo path programs.
• DeLesley S. Hutchins,Pure subtype systems.
• Mohamed Faouzi Atig,Ahmed Bouajjani,Sebastian Burckhardt,Madanlal Musuvathi,On the verification problem for weak memory models.
• Andrzej Filinski,Monads in action.
• Naoki Kobayashi,Naoshi Tabuchi,Hiroshi Unno,Higher-order multi-parameter tree transducers and recursion schemes for program verification.
• Aquinas Hobor,Robert Dockins,Andrew W. Appel,A theory of indirection via approximation.
• Michael Greenberg,Benjamin C. Pierce,Stephanie Weirich,Contracts made manifest.
• Eric Koskinen,Matthew J. Parkinson,Maurice Herlihy,Coarse-grained transactions.
• Tachio Terauchi,Dependent types from counterexamples.
• Philippe Suter,Mirco Dotta,Viktor Kuncak,Decision procedures for algebraic data types with abstractions.
• Stephen Magill,Ming-Hsien Tsai,Peter Lee,Yih-Kuen Tsay,Automatic numeric abstractions for heap-manipulating programs.
• Neil Gershenfeld,David Dalrymple,Kailiang Chen,Ara Knaian,Forrest Green,Erik D. Demaine,Scott Greenwald,Peter Schmidt-Nielsen,Reconfigurable asynchronous logic automata: (RALA).
• Jeremy G. Siek,Philip Wadler,Threesomes, with and without blame.
• Matthias Heizmann,Jochen Hoenicke,Andreas Podelski,Nested interpolants.
• Andrew M. Pitts,Nominal system T.
• Andreas Podelski,Thomas Wies,Counterexample-guided focus.
• Simon J. Gay,Vasco Thudichum Vasconcelos,António Ravara,Nils Gesbert,Alexandre Z. Caldeira,Modular session types for distributed object-oriented programming.
• Adam Chlipala,A verified compiler for an impure functional language.
• Swarat Chaudhuri,Sumit Gulwani,Roberto Lublinerman,Continuity analysis of programs.
• João Dias,Norman Ramsey,Automatically generating instruction selectors using declarative machine descriptions.
• J. Gregory Malecha,Greg Morrisett,Avraham Shinnar,Ryan Wisnesky,Toward a verified relational database management system.
• Martin T. Vechev,Eran Yahav,Greta Yorsh,Abstraction-guided synthesis of synchronization.
• Tobias Wrigstad,Francesco Zappa Nardelli,Sylvain Lebresne,Johan Östlund,Jan Vitek,Integrating typed and untyped code in a scripting language.
• Karthikeyan Bhargavan,Cédric Fournet,Andrew D. Gordon,Modular verification of security protocol code by typing.
• Niklas Broberg,David Sands,Paralocks: role-based information flow control and beyond.
• Max Schäfer,Oege de Moor,Type inference for datalog with complex type hierarchies.
• Patrick Maxim Rondon,Ming Kawaguchi,Ranjit Jhala,Low-level liquid types.
• Magnus O. Myreen,Verified just-in-time compiler on x86.
• Hagit Attiya,G. Ramalingam,Noam Rinetzky,Sequential verification of serializability.
• Trevor Jim,Yitzhak Mandelbaum,David Walker,Semantics and algorithms for data-dependent grammars.
• Steffen Jost,Kevin Hammond,Hans-Wolfgang Loidl,Martin Hofmann,Static determination of quantitative resource usage for higher-order programs.

2009

• Yin Wang,Stéphane Lafortune,Terence Kelly,Manjunath Kudlur,Scott A. Mahlke,The theory of deadlock avoidance via discrete control.
• Sumit Gulwani,Tal Lev-Ami,Mooly Sagiv,A combination framework for tracking partition sizes.
• Ronald Garcia,Andrew Lumsdaine,Amr Sabry,Lazy evaluation and delimited control.
• Roberto Lublinerman,Christian Szegedy,Stavros Tripakis,Modular code generation from synchronous block diagrams: modularity vs. code size.
• Cristiano Calcagno,Dino Distefano,Peter W. O'Hearn,Hongseok Yang,Compositional shape analysis by means of bi-abduction.
• Xinyu Feng,Local rely-guarantee reasoning.
• Xin Qi,Andrew C. Myers,Masked types for sound object initialization.
• Pierre Ganty,Rupak Majumdar,Andrey Rybalchenko,Verifying liveness for asynchronous programs.
• Gilles Barthe,Benjamin Grégoire,Santiago Zanella Béguelin,Formal certification of code-based cryptographic proofs.
• Chris Hawblitzel,Erez Petrank,Automated verification of practical garbage collectors.
• Akimasa Morihata,Kiminori Matsuzaki,Zhenjiang Hu,Masato Takeichi,The third homomorphism theorem on trees: downward & upward lead to divide-and-conquer.
• James Brotherston,Cristiano Calcagno,Classical BI: a logic for reasoning about dualising resources.
• Ben Hardekopf,Calvin Lin,Semi-sparse flow-sensitive pointer analysis.
• Peter A. Jonsson,Johan Nordlander,Positive supercompilation for a higher order call-by-value language.
• Ross Tate,Michael Stepp,Zachary Tatlock,Sorin Lerner,Equality saturation: a new approach to optimization.
• Nathan Grasso Bronson,Christos Kozyrakis,Kunle Olukotun,Feedback-directed barrier optimization in a strongly isolated STM.
• Dana N. Xu,Simon L. Peyton Jones,Koen Claessen,Static contract checking for Haskell.
• David Monniaux,Automatic modular abstractions for linear constraints.
• Julien Brunel,Damien Doligez,René Rydhof Hansen,Julia L. Lawall,Gilles Muller,A foundation for flow-based program matching: using temporal logic and model checking.
• Rachid Guerraoui,Michal Kapalka,The semantics of progress in lock-based transactional memory.
• Daan Leijen,Flexible types: robust type inference for first-class polymorphism.
• Neelakantan R. Krishnaswami,Focusing on pattern matching.
• Alexey Gotsman,Byron Cook,Matthew J. Parkinson,Viktor Vafeiadis,Proving that non-blocking algorithms don't block.
• Akihiko Tozawa,Michiaki Tatsubori,Tamiya Onodera,Yasuhiko Minamide,Copy-on-write in the PHP language.
• Naoki Kobayashi,Types and higher-order recursion schemes for verification of higher-order programs.
• Janis Voigtländer,Bidirectionalization for free! (Pearl).
• Ruy Ley-Wild,Umut A. Acar,Matthew Fluet,A cost semantics for self-adjusting computation.
• Benoît Montagu,Didier Rémy,Modeling abstract types in modules with open existential types.
• Tom Ridge,Verifying distributed systems: the operational approach.
• Jeremy Condit,Brian Hackett,Shuvendu K. Lahiri,Shaz Qadeer,Unifying type checking and property checking for low-level code.
• Sumit Gulwani,Krishna K. Mehra,Trishul M. Chilimbi,SPEED: precise and efficient static estimation of program computational complexity.
• Gérard Boudol,Gustavo Petri,Relaxed memory models: an operational approach.
• Martín Abadi,Gordon D. Plotkin,A model of cooperative threads.
• Susmit Sarkar,Peter Sewell,Francesco Zappa Nardelli,Scott Owens,Tom Ridge,Thomas Braibant,Magnus O. Myreen,Jade Alglave,The semantics of x86-CC multiprocessor machine code.
• Amal Ahmed,Derek Dreyer,Andreas Rossberg,State-dependent representation independence.
• Tayfun Elmas,Shaz Qadeer,Serdar Tasiran,A calculus of atomic actions.

2008

• Wei-Ngan Chin,Cristina David,Huu Hai Nguyen,Shengchao Qin,Enhancing modular OO verification with separation logic.
• Patricia Johann,Neil Ghani,Foundations for structured programming with GADTs.
• Kathleen Fisher,David Walker,Kenny Qili Zhu,Peter White,From dirt to shovels: fully automatic tool generation from ad hoc data.
• Kohei Honda,Nobuko Yoshida,Marco Carbone,Multiparty asynchronous session types.
• Martín Abadi,Andrew Birrell,Tim Harris,Michael Isard,Semantics of transactional memory and automatic mutual exclusion.
• Ashutosh Gupta,Thomas A. Henzinger,Rupak Majumdar,Andrey Rybalchenko,Ru-Gang Xu,Proving non-termination.
• Marius Nita,Dan Grossman,Craig Chambers,A theory of platform-dependent low-level software.
• Marco Gaboardi,Jean-Yves Marion,Simona Ronchi Della Rocca,A logical account of pspace.
• James Brotherston,Richard Bornat,Cristiano Calcagno,Cyclic proofs of program termination in separation logic.
• Janis Voigtländer,Much ado about two (pearl): a pearl on parallel prefix computation.
• Katherine F. Moore,Dan Grossman,High-level small-step operational semantics for transactions.
• Matthew J. Parkinson,Gavin M. Bierman,Separation logic, abstraction and inheritance.
• Umut A. Acar,Amal Ahmed,Matthias Blume,Imperative self-adjusting computation.
• Bor-Yuh Evan Chang,Xavier Rival,Relational inductive shape analysis.
• Greta Yorsh,Eran Yahav,Satish Chandra,Generating precise and concise procedure summaries.
• Hugo Herbelin,Silvia Ghilezan,An approach to call-by-name delimited continuations.
• Sam Tobin-Hochstadt,Matthias Felleisen,The design and implementation of typed scheme.
• Swarat Chaudhuri,Subcubic algorithms for recursive state machines.
• Aaron Bohannon,J. Nathan Foster,Benjamin C. Pierce,Alexandre Pilkiewicz,Alan Schmitt,Boomerang: resourceful lenses for string data.
• Giuseppe Castagna,Nils Gesbert,Luca Padovani,A theory of contracts for web services.
• Noam Zeilberger,Focusing and higher-order abstract syntax.
• Xin Zheng,Radu Rugina,Demand-driven alias analysis for C.
• Andrea Asperti,The intensional content of Rice's theorem.
• Conor McBride,Clowns to the left of me, jokers to the right (pearl): dissecting data structures.
• Peeter Laud,On the computational soundness of cryptographically masked flows.
• Iulian Neamtiu,Michael Hicks,Jeffrey S. Foster,Polyvios Pratikakis,Contextual effects for version-consistent dynamic software updatingalland safe concurrent programming.
• Brian E. Aydemir,Arthur Charguéraud,Benjamin C. Pierce,Randy Pollack,Stephanie Weirich,Engineering formal metatheory.
• Hamed Seiied Alavi,Seth Gilbert,Rachid Guerraoui,Extensible encoding of type hierarchies.
• Jean-Baptiste Tristan,Xavier Leroy,Formal verification of translation validators: a case study on instruction scheduling optimizations.
• Nils Anders Danielsson,Lightweight semiformal time complexity analysis for purely functional data structures.
• Brigitte Pientka,A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions.
• Shuvendu K. Lahiri,Shaz Qadeer,Back to the future: revisiting precise program verification using SMT solvers.
• Christopher Unkel,Monica S. Lam,Automatic inference of stationary fields: a generalization of java's final fields.
• Cédric Fournet,Tamara Rezk,Cryptographically sound implementations for typed information-flow security.
• Sumit Gulwani,Bill McCloskey,Ashish Tiwari,Lifting abstract interpreters to quantified logical domains.

2007

• Dan R. Ghica,Geometry of synthesis: a structured approach to VLSI design.
• Jeffrey Mark Siskind,Barak A. Pearlmutter,First-class nonstandard interpretations by opening closures.
• Cristiano Calcagno,Philippa Gardner,Uri Zarfaty,Context logic as modal logic: completeness and parametric inexpressivity.
• Daniel K. Lee,Karl Crary,Robert Harper,Towards a mechanized metatheory of standard ML.
• Marina Polishchuk,Ben Liblit,Chloë W. Schulze,Dynamic heap type inference for program understanding and debugging.
• Atsushi Ohori,Isao Sasano,Lightweight fusion by fixed point promotion.
• Jacob Matthews,Robert Bruce Findler,Operational semantics for multi-language programs.
• Yitzhak Mandelbaum,Kathleen Fisher,David Walker,Mary F. Fernández,Artem Gleyzer,PADS/ML: a functional data description language.
• Andrew M. Pitts,Mark R. Shinwell,Generative unbinding of names.
• Michele Bugliesi,Marco Giunti,Secure implementations of typed channel abstractions.
• Mila Dalla Preda,Mihai Christodorescu,Somesh Jha,Saumya K. Debray,A semantics-based approach to malware detection.
• Maria Jump,Kathryn S. McKinley,Cork: dynamic memory leak detection for garbage-collected languages.
• Xipeng Shen,Jonathan Shaw,Brian Meeker,Chen Ding,Locality approximation using time.
• Vineet Kahlon,Aarti Gupta,On the analysis of interacting pushdown systems.
• Matthew Might,Logic-flow analysis of higher-order programs.
• Pavel Avgustinov,Elnar Hajiyev,Neil Ongkingco,Oege de Moor,Damien Sereni,Julian Tibble,Mathieu Verbaere,Semantics of static pointcuts in aspectJ.
• Michael Emmi,Jeffrey S. Fischer,Ranjit Jhala,Rupak Majumdar,Lock allocation.
• Kapil Vaswani,Aditya V. Nori,Trishul M. Chilimbi,Preferential path profiling: compactly numbering interesting paths.
• Kristian Støvring,Søren B. Lassen,A complete, co-inductive syntactic theory of sequential control and state.
• Derek Dreyer,Robert Harper,Manuel M. T. Chakravarty,Gabriele Keller,Modular type classes.
• Andrew W. Appel,Paul-André Melliès,Christopher D. Richards,Jérôme Vouillon,A very modal model of a modern, major, general type system.
• Barak A. Pearlmutter,Jeffrey Mark Siskind,Lazy multivariate higher-order forward-mode AD.
• Matthew J. Parkinson,Richard Bornat,Peter W. O'Hearn,Modular verification of a non-blocking stack.
• Harvey Tuch,Gerwin Klein,Michael Norrish,Types, bytes, and separation logic.
• Dachuan Yu,Ajay Chander,Nayeem Islam,Igor Serikov,JavaScript instrumentation for browser security.
• Ranjit Jhala,Rupak Majumdar,Interprocedural analysis of asynchronous programs.
• Josh Berdine,Aziem Chawdhary,Byron Cook,Dino Distefano,Peter W. O'Hearn,Variance analyses from invariance analyses.
• Ben Wiedermann,William R. Cook,Extracting queries by static analysis of transparent persistence.
• Ralf Lämmel,Scrap your boilerplate with XPath-like combinators.
• John H. Reppy,Yingqi Xiao,Specialization of CML message-passing primitives.
• Juan Chen,A typed intermediate language for compiling multiple inheritance.
• Sumit Gulwani,Nebojsa Jojic,Program verification as probabilistic inference.
• Pasquale Malacaria,Assessing security threats of looping constructs.
• Mayur Naik,Alex Aiken,Conditional must not aliasing for static race detection.
• Byron Cook,Alexey Gotsman,Andreas Podelski,Andrey Rybalchenko,Moshe Y. Vardi,Proving that programs eventually do something good.
• Patrice Godefroid,Compositional dynamic test generation.

2006

• Daniel S. Dantas,David Walker,Harmless advice.
• Sebastian Hunt,David Sands,On flow-sensitive security types.
• Shuvendu K. Lahiri,Shaz Qadeer,Verifying properties of well-founded linked lists.
• Jerome Vouillon,Polymorphic regular tree types and patterns.
• François Pottier,Yann Régis-Gianas,Stratified type inference for generalized algebraic data types.
• Mandana Vaziri,Frank Tip,Julian Dolby,Associating synchronization constraints with data in an object-oriented language.
• Torben Amtoft,Sruthi Bandhakavi,Anindya Banerjee,A logic for information flow in object-oriented programs.
• Vasileios Koutavas,Mitchell Wand,Small bisimulations for reasoning about higher-order imperative programs.
• Steve Bishop,Matthew Fairbairn,Michael Norrish,Peter Sewell,Michael Smith,Keith Wansbrough,Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations.
• Ik-Soon Kim,Kwangkeun Yi,Cristiano Calcagno,A polymorphic modal type system for lisp-like multi-staged languages.
• Cormac Flanagan,Hybrid type checking.
• Rajeev Alur,Swarat Chaudhuri,P. Madhusudan,A fixpoint calculus for local and global program flows.
• Gabriel Dos Reis,Bjarne Stroustrup,Specifying C++ concepts.
• Bill McCloskey,Feng Zhou,David Gay,Eric A. Brewer,Autolocker: synchronization inference for atomic sections.
• Guangyu Chen,Feihui Li,Mahmut T. Kandemir,Compiler-directed channel allocation for saving power in on-chip networks.
• Xavier Leroy,Formal certification of a compiler back-end or: programming a compiler with a proof assistant.
• Zhendong Su,Gary Wassermann,The essence of command injection attacks in web applications.
• Albert Cohen,Marc Duranton,Christine Eisenbeis,Claire Pagetti,Florence Plateau,Marc Pouzet,N-synchronous Kahn networks: a relaxed model of synchrony for real-time systems.
• Gautam Gupta,Sanjay V. Rajopadhye,Simplifying reductions.
• Vijay Menon,Neal Glew,Brian R. Murphy,Andrew McCreight,Tatiana Shpeisman,Ali-Reza Adl-Tabatabai,Leaf Petersen,A verifiable SSA program representation for aggressive compiler optimization.
• Zhaozhong Ni,Zhong Shao,Certified assembly programming with embedded code pointers.
• Erik Ernst,Klaus Ostermann,William R. Cook,A virtual class calculus.
• Jed Liu,Aaron Kimball,Andrew C. Myers,Interruptible iterators.
• Matthew Might,Olin Shivers,Environment analysis via Delta CFA.
• Philippe Meunier,Robert Bruce Findler,Matthias Felleisen,Modular set-based analysis from contracts.
• Hayo Thielecke,Frame rules from answer types for code pointers.
• Mads Dam,Decidability and proof systems for language-based noninterference relations.
• Norman Danner,James S. Royer,Adventures in time and space.
• Kathleen Fisher,Yitzhak Mandelbaum,David Walker,The next 700 data description languages.
• Reuben Olinsky,Christian Lindig,Norman Ramsey,Staged allocation: a compositional technique for specifying and implementing procedure calling conventions.
• Yi Lu,John Potter,Protecting representation with effect encapsulation.
• Chengliang Zhang,Chen Ding,Mitsunori Ogihara,Yutao Zhong,Youfeng Wu,A hierarchical model of data locality.
• Nils Anders Danielsson,John Hughes,Patrik Jansson,Jeremy Gibbons,Fast and loose reasoning is morally correct.

2005

• Healfdene Goguen,A syntactic approach to eta equality in type theory.
• Sungwoo Park,Frank Pfenning,Sebastian Thrun,A probabilistic language based upon sampling functions.
• Matthias Neubauer,Peter Thiemann,From sequential programs to multi-tier applications by program transformation.
• Dan R. Ghica,Slot games: a quantitative model of computation.
• Haruo Hosoya,Alain Frisch,Giuseppe Castagna,Parametric polymorphism for XML.
• Cristiano Calcagno,Philippa Gardner,Uri Zarfaty,Context logic and tree update.
• Gareth Stoyle,Michael W. Hicks,Gavin M. Bierman,Peter Sewell,Iulian Neamtiu,Mutatis mutandis: safe and predictable dynamic software updating.
• Matthew J. Parkinson,Gavin M. Bierman,Separation logic and abstraction.
• Peng Li,Steve Zdancewic,Downgrading policies and relaxed noninterference.
• John Tang Boyland,William Retert,Connecting effects and uniqueness with adoption.
• Brian Hackett,Radu Rugina,Region-based shape analysis with tracked locations.
• Eijiro Sumii,Benjamin C. Pierce,A bisimulation for type abstraction and recursion.
• Jeremy Manson,William Pugh,Sarita V. Adve,The Java memory model.
• Noam Rinetzky,Jörg Bauer,Thomas W. Reps,Shmuel Sagiv,Reinhard Wilhelm,A semantics for procedure local heaps and its abstractions.
• Juan Chen,David Tarditi,A simple typed intermediate language for object-oriented languages.
• Yichen Xie,Alexander Aiken,Scalable error detection using boolean satisfiability.
• Rajeev Alur,Pavol Cerný,P. Madhusudan,Wonhong Nam,Synthesis of interface specifications for Java classes.
• Simon J. Gay,Rajagopal Nagarajan,Communicating quantum processes.
• Orna Grumberg,Flavio Lerda,Ofer Strichman,Michael Theobald,Proof-guided underapproximation-widening for multi-process systems.
• Jens Palsberg,Martín Abadi,Manuel M. T. Chakravarty,Gabriele Keller,Simon L. Peyton Jones,Simon Marlow,Associated types with class.
• Sumit Gulwani,George C. Necula,Precise interprocedural analysis using random interpretation.
• Sorin Lerner,Todd D. Millstein,Erika Rice,Craig Chambers,Automated soundness proofs for dataflow analyses and transformations via local rules.
• Cormac Flanagan,Patrice Godefroid,Dynamic partial-order reduction for model checking software.
• J. Nathan Foster,Michael B. Greenwald,Jonathan T. Moore,Benjamin C. Pierce,Alan Schmitt,Combinators for bi-directional tree transformations: a linguistic approach to the view update problem.
• Richard Cobbe,Matthias Felleisen,Environmental acquisition revisited.
• Denis Gopan,Thomas W. Reps,Shmuel Sagiv,A framework for numeric analysis of array operations.
• Roberto Bruni,Hernán C. Melgratti,Ugo Montanari,Theoretical foundations for compensations in flow composition languages.
• John Field,Carlos A. Varela,Transactors: a programming model for maintaining globally consistent distributed state in unreliable environments.
• Davide Ancona,Ferruccio Damiani,Sophia Drossopoulou,Elena Zucca,Polymorphic bytecode: compositional compilation for Java-like languages.
• Richard Bornat,Cristiano Calcagno,Peter W. O'Hearn,Matthew J. Parkinson,Permission accounting in separation logic.
• Andreas Podelski,Andrey Rybalchenko,Transition predicate abstraction and fair termination.

2004

• Eijiro Sumii,Benjamin C. Pierce,A bisimulation for dynamic sealing.
• Shaz Qadeer,Sriram K. Rajamani,Jakob Rehof,Summarizing procedures in concurrent programs.
• Thomas A. Henzinger,Ranjit Jhala,Rupak Majumdar,Kenneth L. McMillan,Abstractions from proofs.
• François Pottier,Nadji Gauthier,Polymorphic typed defunctionalization.
• Davide Ancona,Elena Zucca,Principal typings for Java-like languages.
• Cormac Flanagan,Stephen N. Freund,Atomizer: a dynamic atomicity checker for multithreaded programs.
• Nobuko Yoshida,Channel dependent types for higher-order mobile processes.
• Patrick Cousot,Radhia Cousot,An abstract interpretation-based framework for software watermarking.
• Hans-Juergen Boehm,The space cost of lazy reference counting.
• Nick Benton,Simple relational correctness proofs for static analyses and program transformations.
• Denis Caromel,Ludovic Henrio,Bernard P. Serpette,Asynchronous and deterministic objects.
• Lars Birkedal,Noah Torp-Smith,John C. Reynolds,Local reasoning about a copying garbage collector.
• Patricia Johann,Janis Voigtländer,Free theorems in the presence of seq.
• Karthikeyan Bhargavan,Cédric Fournet,Andrew D. Gordon,A semantics for web services authentication.
• Derek Dreyer,A type system for well-founded recursion.
• Ganesh Sittampalam,Oege de Moor,Ken Friis Larsen,Incremental execution of transformation specifications.
• Sriram Sankaranarayanan,Henny Sipma,Zohar Manna,Non-linear loop invariant generation using Gröbner bases.
• Marcelo P. Fiore,Isomorphisms of generic recursive polynomial types.
• Silvano Dal-Zilio,Denis Lugiez,Charles Meyssonnier,A logic you can count on.
• Roberto Giacobazzi,Isabella Mastroeni,Abstract non-interference: parameterizing non-interference by abstract interpretation.
• Joshua Dunfield,Frank Pfenning,Tridirectional typechecking.
• Vincent Balat,Roberto Di Cosmo,Marcelo P. Fiore,Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums.
• Sumit Gulwani,George C. Necula,Global value numbering using random interpretation.
• Neil D. Jones,Xavier Leroy,Xavier Rival,Symbolic transfer function-based approaches to certified compilation.
• Markus Müller-Olm,Helmut Seidl,Precise interprocedural analysis through linear algebra.
• Bryan Ford,Parsing expression grammars: a recognition-based syntactic foundation.
• Peter W. O'Hearn,Hongseok Yang,John C. Reynolds,Separation and information hiding.
• Dachuan Yu,Andrew Kennedy,Don Syme,Formalization of generics for the .NET common language runtime.
• Jerome Vouillon,Paul-André Melliès,Semantic types: a fresh look at the ideal model for types.

2003

• Leaf Petersen,Robert Harper,Karl Crary,Frank Pfenning,A type theory for memory allocation and data layout.
• Larry Carter,Jeanne Ferrante,Clark D. Thomborson,Folklore confirmed: reducible flow graphs are exponentially larger.
• Hayo Thielecke,From control effects to typed continuation passing.
• Sriraman Tallam,Rajiv Gupta,Bitwidth aware global register allocation.
• Ahmed Bouajjani,Javier Esparza,Tayssir Touili,A generic approach to the static analysis of concurrent programs with procedures.
• Alex Aiken,Greg Morrisett,Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New Orleans, Louisisana, USA, January 15-17, 2003.
• Yoav Zibin,Joseph Gil,Jeffrey Considine,Efficient algorithms for isomorphisms of simple types.
• Ovidiu Gheorghioiu,Alexandru Salcianu,Martin C. Rinard,Interprocedural compatibility analysis for static object preallocation.
• Thomas Ball,Mayur Naik,Sriram K. Rajamani,From symptom to cause: localizing errors in counterexample traces.
• Ole Høgh Jensen,Robin Milner,Bigraphs and transitions.
• Karl Crary,Toward a foundational typed assembly language.
• Gang Chen,Coercive subtyping for the calculus of constructions.
• Martin Hofmann,Steffen Jost,Static prediction of heap space usage for first-order functional programs.
• Sumit Gulwani,George C. Necula,Discovering affine equalities using random interpretation.
• Walid Taha,Michael Florentin Nielsen,Environment classifiers.
• Venkatesan T. Chakaravarthy,New results on the computability and complexity of points - to analysis.
• Alan Schmitt,Jean-Bernard Stefani,The m-calculus: a higher-order distributed process calculus.
• Yoav Zibin,Joseph Gil,Incremental algorithms for dispatching in dynamically typed languages.
• Umut A. Acar,Guy E. Blelloch,Robert Harper,Selective memoization.
• David F. Bacon,Perry Cheng,V. T. Rajan,A real-time garbage collector with low overhead and consistent utilization.
• Gilles Barthe,Horatiu Cirstea,Claude Kirchner,Luigi Liquori,Pure patterns type systems.
• Hongwei Xi,Chiyan Chen,Gang Chen,Guarded recursive datatype constructors.
• Chandrasekhar Boyapati,Barbara Liskov,Liuba Shrira,Ownership types for object encapsulation.
• Jérôme Siméon,Philip Wadler,The essence of XML.
• Hans-Juergen Boehm,Destructors, finalizers, and synchronization.
• Derek Dreyer,Karl Crary,Robert Harper,A type system for higher-order modules.

2002

• Patrick Cousot,Radhia Cousot,Systematic design of program transformation frameworks by abstract interpretation.
• Viktor Kuncak,Patrick Lam,Martin C. Rinard,Role analysis.
• Sorin Lerner,David Grove,Craig Chambers,Composing dataflow analyses and transformations.
• George C. Necula,Scott McPeak,Westley Weimer,CCured: type-safe retrofitting of legacy code.
• Matthai Philipose,Craig Chambers,Susan J. Eggers,Towards automatic construction of staged compilers.
• Atsushi Igarashi,Naoki Kobayashi,Resource usage analysis.
• Matthias Neubauer,Peter Thiemann,Martin Gasbichler,Michael Sperber,Functional logic overloading.
• Zhendong Su,Alexander Aiken,Joachim Niehren,Tim Priesnitz,Ralf Treinen,The first-order theory of subtyping constraints.
• Zhong Shao,Bratin Saha,Valery Trifonov,Nikolaos Papaspyrou,A type system for certified binaries.
• Kohei Honda,Nobuko Yoshida,A uniform type structure for secure information flow.
• Glenn Ammons,Rastislav Bodík,James R. Larus,Mining specifications.
• François Pottier,Vincent Simonet,Information flow inference for ML.
• Norman Ramsey,Avi Pfeffer,Stochastic lambda calculus and monads of probability distributions.
• Hans-Juergen Boehm,Bounding space usage of conservative garbage collectors.
• Yefim Shuf,Manish Gupta,Rajesh Bordawekar,Jaswinder Pal Singh,Exploiting prolific types for memory management and optimizations.
• Shai Rubin,Rastislav Bodík,Trishul M. Chilimbi,An efficient profile-analysis framework for data-layout optimizations.
• Cédric Fournet,Andrew D. Gordon,Stack inspection: theory and variants.
• Massimo Merro,Matthew Hennessy,Bisimulation congruences in safe ambients.
• Sagar Chaki,Sriram K. Rajamani,Jakob Rehof,Types as models: model checking message-passing programs.
• Martín Abadi,Bruno Blanchet,Analyzing security protocols with secrecy types and logic programs.
• John Launchbury,John C. Mitchell,Conference Record of POPL 2002: The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002.
• Anindya Banerjee,David A. Naumann,Representation independence, confinement and access control [extended abstract].
• Thomas A. Henzinger,Ranjit Jhala,Rupak Majumdar,Grégoire Sutre,Lazy abstraction.
• David Lacey,Neil D. Jones,Eric Van Wyk,Carl Christian Frederiksen,Proving correctness of compiler optimizations by temporal logic.
• Erez Petrank,Dror Rawitz,The hardness of cache conscious data placement.
• Cormac Flanagan,Shaz Qadeer,Predicate abstraction for software verification.
• Umut A. Acar,Guy E. Blelloch,Robert Harper,Adaptive functional programming.
• Martin Hofmann,The strength of non-size increasing computation.

2001

• Andrew D. Gordon,Don Syme,Typing a multi-language intermediate code.
• Cormac Flanagan,James B. Saxe,Avoiding exponential explosion: generating compact verification conditions.
• Chin Soon Lee,Neil D. Jones,Amir M. Ben-Amram,The size-change principle for program termination.
• George C. Necula,Shree Prakash Rahul,Oracle-based checking of untrusted software.
• David Monniaux,An abstract Monte-Carlo method for the analysis of probabilistic programs.
• Karthikeyan Bhargavan,Satish Chandra,Peter J. McCann,Carl A. Gunter,What packets may come: automata for network monitoring.
• Martin Odersky,Christoph Zenger,Matthias Zenger,Colored local type inference.
• Mark Shields,Erik Meijer,Type-indexed rows.
• Atsushi Igarashi,Naoki Kobayashi,A generic type system for the Pi-calculus.
• Daniel C. Wang,Andrew W. Appel,Type-preserving garbage collectors.
• Davide Sangiorgi,Extensionality and Intensionality of the Ambient Logics.
• Michele Bugliesi,Giuseppe Castagna,Secure safe ambients.
• Martín Abadi,Cédric Fournet,Mobile values, new names, and secure communication.
• Mahmut T. Kandemir,A compiler technique for improving whole-program locality.
• Jakob Rehof,Manuel Fähndrich,Type-base flow analysis: from polymorphic subtyping to CFL-reachability.
• Haruo Hosoya,Benjamin C. Pierce,Regular expression pattern matching for XML.
• Jerome Vouillon,Combining subsumption and binary methods: an object calculus with views.
• Cristiano Calcagno,Stratified operational semantics for safety and correctness of the region calculus.
• Asis Unyapoth,Peter Sewell,Nomadic pict: correct communication infrastructure for mobile computation.
• Joseph Gil,Subtyping arithmetical types.
• Chris Hankin,Dave Schmidt,Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001.
• Eran Yahav,Verifying safety properties of concurrent Java programs using 3-valued logic.
• Peter Sewell,Modules, abstract types, and distributed versioning.
• Samin S. Ishtiaq,Peter W. O'Hearn,BI as an Assertion Language for Mutable Data Structures.

2000

• Robert Muth,Saumya K. Debray,On the Complexity of Flow-Sensitive Dataflow Analyses.
• Dennis M. Volpano,Geoffrey Smith,Verifying Secrets and Relative Secrecy.
• Mark N. Wegman,Thomas W. Reps,Javier Esparza,Andreas Podelski,Efficient Algorithms for pre* and post* on Interprocedural Parallel Flow Graphs.
• Ben Liblit,Alexander Aiken,Type Systems for Distributed Data Structures.
• Christopher A. Stone,Robert Harper,Deciding Type Equivalence with Singleton Kinds.
• David Walker,A Type System for Expressive Security Policies.
• Nevin Heintze,Joxan Jaffar,Razvan Voicu,A Framework for Combining Analysis and Verification.
• Zhendong Su,Manuel Fähndrich,Alexander Aiken,Projection Merging: Reducing Redundancies in Inclusion Constraint Graphs.
• Francesca Levi,Davide Sangiorgi,Controlling Interference in Ambients.
• Carl A. Gunter,Trevor Jim,Generalized Certificate Revocation.
• Raghavan Komondoor,Susan Horwitz,Semantics-Preserving Procedure Extraction.
• Patrick Cousot,Radhia Cousot,Temporal Abstract Interpretation.
• Hanne Riis Nielson,Flemming Nielson,Shape Analysis for Mobile Ambients.
• Todd B. Knoblock,Jakob Rehof,Type Elaboration and Subtype Completion for Java Bytecode.
• Thomas Colcombet,Pascal Fradet,Enforcing Trace Properties by Program Transformation.
• Oliver Rüthing,Jens Knoop,Bernhard Steffen,Sparse Code Motion.
• Karl Crary,Stephanie Weirich,Resource Bound Certification.
• Anders Sandholm,Michael I. Schwartzbach,A Type System for Dynamic Web Documents.
• Andrea Asperti,Paolo Coppola,Simone Martini,(Optimal) Duplication is not Elementary Recursive.
• Alan Bawden,First-Class Macros have Types.
• Timothy J. Hickey,Analytic Constraint Solving and Interval Arithmetic.
• Craig Chambers,Bill Harrison,John M. Vlissides,A Debate on Language and Tool Support for Design Patterns.
• Johan Agat,Transforming Out Timing Leaks.
• Witold Charatonik,Andreas Podelski,Jean-Marc Talbot,Paths vs. Trees in Set-Based Program Analysis.
• Luca Cardelli,Andrew D. Gordon,Anytime, Anywhere: Modal Logics for Mobile Ambients.
• Jeffrey R. Lewis,John Launchbury,Erik Meijer,Mark Shields,Implicit Parameters: Dynamic Scoping with Static Types.
• Ralf Hinze,A New Approach to Generic Functional Programming.
• Andrew W. Appel,Amy P. Felty,A Semantic Model of Types and Machine Instuctions for Proof-Carrying Code.
• Rajeev Alur,Radu Grosu,Modular Refinement of Hierarchic Reactive Machines.
• Martín Abadi,Cédric Fournet,Georges Gonthier,Authentication Primitives and Their Compilation.
• Yoo C. Chung,Soo-Mook Moon,Kemal Ebcioglu,Dan Sahlin,Reducing Sweep Time for a Nearly Empty Heap.

1999

• Shmuel Sagiv,Thomas W. Reps,Reinhard Wilhelm,Parametric Shape Analysis via 3-Valued Logic.
• Neal Glew,J. Gregory Morrisett,Type-Safe Linking and Modular Assembly Language.
• Naoki Kobayashi,Quasi-Linear Types.
• Andrew C. Myers,JFlow: Practical Mostly-Static Information Flow Control.
• Robert O'Callahn,A Simple, Comprehensive Type System for Java Bytecode Subroutines.
• Oscar Waddell,R. Kent Dybvig,Extending the Scope of Syntactic Abstraction.
• Christian S. Collberg,Clark D. Thomborson,Software Watermarking: Models and Dynamic Embeddings.
• M. Anton Ertl,Optimal Code Selection in DAGs.
• Martin Ruckert,Continuous Grammars.
• Andrzej Filinski,Representing Layered Monads.
• A. J. Kfoury,J. B. Wells,Principality and Decidable Type Inference for Finite-Rank Intersection Types.
• James Riely,Matthew Hennessy,Trust and Partial Typing in Open Systems of Mobile Agents.
• Phillip M. Yelland,A Compositional Account of the Java Virtual Machine.
• G. Ramalingam,John Field,Frank Tip,Aggregate Structure Identification and Its Application to Program Analysis.
• Peter Harry Eidorff,Fritz Henglein,Christian Mossin,Henning Niss,Morten Heine Sørensen,Mads Tofte,AnnoDomini: From Type Theory to Year 2000 Conversion Tool.
• Vineet Gupta,Radha Jagadeesan,Prakash Panangaden,Stochastic Processes as Concurrent Constraint Programs.
• Andrew Moran,David Sands,Improvement in a Lazy Context: An Operational Theory for Call-by-Need.
• Luca Cardelli,Andrew D. Gordon,Types for Mobile Ambients.
• Hongwei Xi,Frank Pfenning,Dependent Types in Practical Programming.
• Martín Abadi,Anindya Banerjee,Nevin Heintze,Jon G. Riecke,A Core Calculus of Dependency.
• Mitchell Wand,Igor Siveroni,Constraint Systems for Useless Variable Elimination.
• Karl Crary,David Walker,J. Gregory Morrisett,Typed Memory Management in a Calculus of Capabilities.
• Ramkrishna Chatterjee,Barbara G. Ryder,William Landi,Relevant Context Inference.
• François Pessaux,Xavier Leroy,Type-Based Analysis of Uncaught Exceptions.
• Keith Wansbrough,Simon L. Peyton Jones,Once Upon a Polymorphic Type.

1998

• Rakesh Ghiya,Laurie J. Hendren,Putting Pointer Analysis to Work.
• Christian S. Collberg,Clark D. Thomborson,Douglas Low,Manufacturing Cheap, Resilient, and Stealthy Opaque Constructs.
• Denis Barthou,Albert Cohen,Jean-Francois Collard,Maximal Static Expansion.
• David B. MacQueen,Luca Cardelli,John Hannan,Patrick Hicks,Higher-Order unCurrying.
• Jens Palsberg,Christina Pavlopoulou,From Polyvariant Flow Information to Intersection and Union Types.
• Zhenjiang Hu,Masato Takeichi,Wei-Ngan Chin,Parallelization in Calculational Forms.
• Benjamin C. Pierce,David N. Turner,Local Type Inference.
• Alexander Aiken,David Gay,Barrier Inference.
• Nevin Heintze,Jon G. Riecke,The SLam Calculus: Programming with Secrecy and Integrity.
• J. Gregory Morrisett,David Walker,Karl Crary,Neal Glew,From System F to Typed Assembly Language.
• Bruno Blanchet,Escape Analysis: Correctness Proof, Implementation and Experimental Results.
• Rastislav Bodík,Sadun Anik,Path-Sensitive Value-Flow Analysis.
• David A. Schmidt,Data Flow Analysis is Model Checking of Abstract Interpretations.
• Xavier Leroy,François Rouaix,Security Properties of Typed Applets.
• Yasuhiko Minamide,A Functional Representation of Data Structures with a Hole.
• Tobias Nipkow,David von Oheimb,Javalight is Type-Safe - Definitely.
• Susumu Nishimura,Static Typing for Dynamic Messages.
• Mark Shields,Tim Sheard,Simon L. Peyton Jones,Dynamic Typing as Staged Type Inference.
• James Riely,Matthew Hennessy,A Typed Language for Distributed Mobile Processes (Extended Abstract).
• Andrea Asperti,Harry G. Mairson,Parallel Beta Reduction is not Elementary Recursive.
• Raymie Stata,Martín Abadi,A Type System for Java Bytecode Subroutines.
• Aleksy Schubert,Second-Order Unification and Type Inference for Church-Style Polymorphism.
• Suresh Jagannathan,Peter Thiemann,Stephen Weeks,Andrew K. Wright,Single and Loving It: Must-Alias Analysis for Higher-Order Languages.
• Kathleen Knobe,Vivek Sarkar,Array SSA Form and Its Use in Parallelization.
• Saumya K. Debray,Robert Muth,Matthew Weippert,Alias Analysis of Executable Code.
• Zena M. Ariola,Amr Sabry,Correctness of Monadic State: An Imperative Call-by-Need Calculus.
• Greg DeFouw,David Grove,Craig Chambers,Fast Interprocedural Class Analysis.
• Thomas Ball,Peter Mataga,Shmuel Sagiv,Edge Profiling versus Path Profiling: The Showdown.
• Matthew Flatt,Shriram Krishnamurthi,Matthias Felleisen,Classes and Mixins.
• Geoffrey Smith,Dennis M. Volpano,Secure Information Flow in a Multi-Threaded Imperative Language.
• Simon L. Peyton Jones,Mark Shields,John Launchbury,Andrew P. Tolmach,Bridging the Gulf: A Common Intermediate Language for ML and Haskell.
• Thomas P. Jensen,Inference of Polymorphic and Conditional Strictness Properties.

1997

• Alain Deutsch,On the Complexity of Escape Analysis.
• Sandip K. Biswas,A Demand-Driven Set-Based Analysis.
• Robert Paige,Zhe Yang,High Level Reading and Data Structure Compilation.
• Didier Rémy,Jerome Vouillon,Objective ML: A Simple Object-Oriented Extension of ML.
• Catuscia Palamidessi,Comparing the Expressive Power of the Synchronous and the Asynchronous pi-calculus.
• Amy W. Lim,Monica S. Lam,Maximizing Parallelism and Minimizing Synchronization with Affine Transforms.
• Patrice Godefroid,Model Checking for Programming Languages using Verisoft.
• François Bourdoncle,Stephan Merz,Type-Checking Higher-Order Polymorphic Multi-Methods.
• Patrik Jansson,Johan Jeuring,Polyp - A Polytypic Programming Language.
• Andrew C. Myers,Joseph A. Bank,Barbara Liskov,Parameterized Types for Java.
• Michael Hanus,A Unified Computation Model for Functional and Logic Programming.
• Patrick Cousot,Types as Abstract Interpretations.
• Jakob Rehof,Minimal Typings in Atomic Subtyping.
• Benjamin C. Pierce,Davide Sangiorgi,Behavioral Equivalence in the Polymorphic Pi-calculus.
• Krzysztof R. Apt,Andrea Schaerf,Search and Imperative Programming.
• Erik Ruf,Partitioning Dataflow Analyses Using Types.
• Pascal Fradet,Daniel Le Métayer,Shape Types.
• Mitchell Wand,Gregory T. Sullivan,Denotational Semantics Using an Operationally-Based Term Model.
• Andrew Kennedy,Relational Parametricity and Units of Measure.
• Helmut Seidl,Morten Heine Sørensen,Constraints to Stop Higher-Order Deforestation.
• Luca Cardelli,Program Fragments, Linking, and Modularization.
• David Sands,From SOS Rules to Proof Principles: An Operational Metatheory for Functional Languages.
• Chih-Ping Chen,Paul Hudak,Rolling Your Own MADT - A Connection Between Linear Types and Monads.
• Michael P. Plezbert,Ron Cytron,Is "Just in Time" = "Better Late than Never"?
• Gérard Boudol,The Pi-calculus in Direct Style.
• Pedro C. Diniz,Martin C. Rinard,Synchronization Transformations for Parallel Computing.
• Marc Shapiro,Susan Horwitz,Fast and Accurate Flow-Insensitive Points-To Analysis.
• Amokrane Saïbi,Typing Algorithm in Type Theory with Inheritance.
• George C. Necula,Proof-Carrying Code.
• Mark P. Jones,First-class Polymorphism with Type Inference.
• C.-H. Luke Ong,Charles A. Stewart,A Curry-Howard Foundation for Functional Computation with Control.
• Alberto Pettorossi,Maurizio Proietti,Sophie Renault,Reducing Nondeterminism while Specializing Logic Programs.
• Martin Odersky,Philip Wadler,Pizza into Java: Translating Theory into Practice.
• Karin Högstedt,Larry Carter,Jeanne Ferrante,Determining the Idle Time of a Tiling.
• David Lesens,Nicolas Halbwachs,Pascal Raymond,Automatic Verification of Parameterized Linear Networks of Processes.
• Hanne Riis Nielson,Flemming Nielson,Infinitary Control Flow Analysis: a Collecting Semantics for Closure Analysis.
• Aart Middeldorp,Call by Need Computations to Root-Stable Form.

1996

• Trevor Jim,What Are Principal Typings and What Are They Good For?
• J. Michael Ashley,A Practical and Flexible Flow Analysis for Higher-Order Languages.
• Manish Gupta,Edith Schonberg,Static Analysis to Reduce Synchronization Costs in Data-Parallel Programs.
• Olivier Danvy,Type-Directed Partial Evaluation.
• Yanhong A. Liu,Scott D. Stoller,Tim Teitelbaum,Discovering Auxiliary Information for Incremental Computation.
• Leonidas Fegaras,Tim Sheard,Revisiting Catamorphisms over Datatypes with Embedded Functions (or, Programs from Outer Space).
• Rowan Davies,Frank Pfenning,A Modal Analysis of Staged Computation.
• Steven M. Kurlander,Charles N. Fischer,Minimum Cost Interprocedural Register Allocation.
• Nicholas Pippenger,Pure versus Impure LISP.
• Cédric Fournet,Georges Gonthier,The Reflexive CHAM and the Join-Calculus.
• Andrea Asperti,On the Complexity of Beta-Reduction.
• Dawson R. Engler,Wilson C. Hsieh,M. Frans Kaashoek,`C: A Language for High-Level, Efficient, and Machine-Independent Dynamic Code Generation.
• Andrew D. Gordon,Gareth D. Rees,Bisimilarity for a First-Order Calculus of Objects with Subtyping.
• Lal George,Andrew W. Appel,Iterated Register Coalescing.
• Shmuel Sagiv,Thomas W. Reps,Reinhard Wilhelm,Solving Shape-Analysis Problems in Languages with Destructive Updating.
• Kohei Honda,Composing Processes.
• Yasuhiko Minamide,J. Gregory Morrisett,Robert Harper,Typed Closure Conversion.
• Roger Hoover,F. Kenneth Zadeck,Generating Machine Specific Optimizing Compilers.
• Todd A. Proebsting,Scott A. Watterson,Filter Fusion.
• Rakesh Ghiya,Laurie J. Hendren,Is it a Tree, a DAG, or a Cyclic Graph? A Shape Analysis for Heap-Directed Pointers in C.
• Mark P. Jones,Using Parameterized Signatures to Express Modular Structure.
• Martín Abadi,Luca Cardelli,Ramesh Viswanathan,An Interpretation of Objects and Object Types.
• John Hughes,Lars Pareto,Amr Sabry,Proving the Correctness of Reactive Systems Using Sized Types.
• Bjarne Steensgaard,Points-to Analysis in Almost Linear Time.
• Lars Birkedal,Mads Tofte,Magnus Vejlstrup,From Region Inference to von Neumann Machines via Region Representation Inference.
• John Greiner,Guy E. Blelloch,A Provably Time-Efficient Parallel Implementation of Full Speculation.
• Martin Odersky,Konstantin Läufer,Putting Type Annotations to Work.
• Joachim Niehren,Functional Computation as Concurrent Computation.
• Daniel Jackson,Somesh Jha,Craig Damon,Faster Checking of Software Specifications by Eliminating Isomorphs.
• Charles Consel,François Noël,A General Approach for Run-Time Specialization and its Application to C.
• Christopher Colby,Peter Lee,Trace-Based Program Analysis.
• Simon L. Peyton Jones,Andrew D. Gordon,Sigbjorn Finne,Concurrent Haskell.
• Kannan Govindarajan,Bharat Jayaraman,Surya Mantha,Optimization and Relaxation in Constraint Logic Languages.
• Naoki Kobayashi,Benjamin C. Pierce,David N. Turner,Linearity and the Pi-Calculus.

1995

• Mark W. Bailey,Jack W. Davidson,A Formal Model of Procedure Calling Conventions.
• Sergei G. Vorobyov,Structural Decidable Extensions of Bounded Quantification.
• John C. Reynolds,Using Functor Categories to Generate Intermediate Code.
• Luca Cardelli,A Language with Distributed Scope.
• John Field,G. Ramalingam,Frank Tip,Parametric Program Slicing.
• Vugranam C. Sreedhar,Guang R. Gao,A Linear Time Algorithm for Placing phi-nodes.
• Jon G. Riecke,Ramesh Viswanathan,Isolating Side Effects in Sequential Languages.
• Zena M. Ariola,Matthias Felleisen,John Maraist,Martin Odersky,Philip Wadler,The Call-by-Need Lambda Calculus.
• Steven Dawson,C. R. Ramakrishnan,I. V. Ramakrishnan,Konstantinos F. Sagonas,Steven Skiena,Terrance Swift,David Scott Warren,Unification Factoring for Efficient Execution of Logic Programs.
• Sheng Liang,Paul Hudak,Mark P. Jones,Monad Transformers and Modular Interpreters.
• Sandip K. Biswas,Higher-Order Functors with Transparent Signatures.
• Cormac Flanagan,Matthias Felleisen,The Semantics of Future and Its Use in Program Optimizations.
• Catherine Dubois,François Rouaix,Pierre Weis,Generic Polymorphism.
• E. Allen Emerson,Kedar S. Namjoshi,Reasoning about Rings.
• Klaus E. Schauser,David E. Culler,Seth Copen Goldstein,Separation Constraint Partitioning - A New Algorithm for Partitioning Non-strict Programs into Sequential Threads.
• Ian Mackie,The Geometry of Interaction Machine.
• Stephen D. Brookes,Denis Dancanet,Sequential Algorithms, Deterministic Parallelism, and Intensional Expressiveness.
• Evelyn Duesterwald,Rajiv Gupta,Mary Lou Soffa,Demand-driven Computation of Interprocedural Data Flow.
• Suresh Jagannathan,Stephen Weeks,A Unified Treatment of Flow Analysis in Higher-Order Languages.
• Patrick M. Sansom,Simon L. Peyton Jones,Time and Space Profiling for Non-Strict Higher-Order Functional Languages.
• David Sands,Total Correctness by Local Improvement in Program Transformation.
• Robert Harper,J. Gregory Morrisett,Compiling Polymorphism Using Intensional Type Analysis.
• Rita Altucher,William Landi,An Extended Form of Must Alias Analysis for Dynamic Allocation.
• David J. King,John Launchbury,Structuring Depth-First Search Algorithms in Haskell.
• Xavier Leroy,Applicative Functors and Fully Transparent Higher-Order Modules.
• Vijay A. Saraswat,Radha Jagadeesan,Vineet Gupta,Default Timed Concurrent Constraint Programming.
• Jens Palsberg,Patrick O'Keefe,A Type System Equivalent to Flow Analysis.
• Todd A. Proebsting,Optimizing an ANSI C Interpreter with Superoperators.
• Ahmed Bouajjani,Rachid Echahed,Peter Habermehl,Verifying Infinite State Processes with Sequential and Parallel Composition.
• Bard Bloom,Structured Operational Semantics as a Specification Language.
• Martin Hofmann,Benjamin C. Pierce,Positive Subtyping.
• My Hoang,John C. Mitchell,Lower Bounds on Type Inference with Subtypes.
• John Plevyak,Xingbin Zhang,Andrew A. Chien,Obtaining Sequential Efficiency for Concurrent Object-Oriented Languages.
• Thomas W. Reps,Susan Horwitz,Shmuel Sagiv,Precise Interprocedural Dataflow Analysis via Graph Reachability.

1994

• Damien Doligez,Georges Gonthier,Portable, Unobtrusive Garbage Collection for Multiprocessor Systems.
• Martin Odersky,A Functional Theory of Local Names.
• Mads Tofte,Jean-Pierre Talpin,Implementation of the Typed Call-by-Value lambda-Calculus using a Stack of Regions.
• John Boyland,Susan L. Graham,Composing Tree Attributions.
• Robert Harper,Mark Lillibridge,A Type-Theoretic Approach to Higher-Order Modules with Sharing.
• Frank S. de Boer,Maurizio Gabbrielli,Elena Marchiori,Catuscia Palamidessi,Proving Concurrent Constraint Programs Correct.
• Kim Marriott,Maria J. García de la Banda,Manuel V. Hermenegildo,Analyzing Logic Programs with Dynamic Scheduling.
• Brad Calder,Dirk Grunwald,Reducing Indirect Function call Overhead in C++ Programs.
• Satish Thatté,Automated Synthesis of Interface Adapters for Reusable Classes.
• John Hatcliff,Olivier Danvy,A Generic Account of Continuation-Passing Styles.
• Fritz Henglein,Jesper Jørgensen,Formally Optimal Boxing.
• Agostino Cortesi,Baudouin Le Charlier,Pascal Van Hentenryck,Combinations of Abstract Domains for Logic Programming.
• Sergio Antoy,Rachid Echahed,Michael Hanus,A Needed Narrowing Strategy.
• Vadim Maslov,Lazy Array Data-Flow Dependence Analysis.
• Alexander Aiken,Edward L. Wimmers,T. K. Lakshman,Soft Typing with Conditional Types.
• Pierre Lescanne,From Lambda-sigma to Lambda-upsilon a Journey Through Calculi of Explicit Substitutions.
• Koenraad De Bosschere,Saumya K. Debray,David Gudeman,Sampath Kannan,Call Forwarding: A Simple Interprocedural Optimization Technique for Dynamically Typed Languages.
• Rance Cleaveland,Daniel Yankelevich,An Operational Framework for Value-Passing Processes.
• Jukka Paakki,Multi-Pass Execution of Functional Logic Programs.
• Xavier Leroy,Manifest Types, Modules, and Separate Compilation.
• Robert Muller,A Staging Calculus and its Application to the Verification of Translators.
• Andrzej Filinski,Representing Monads.
• Mitchell Wand,Paul Steckler,Selective and Lightweight Closure Conversion.
• Chris Hankin,Daniel Le Métayer,Deriving Algorithms From Type Inference Systems: Application to Strictness Analysis.
• Jacques Garrigue,Hassan Aït-Kaci,The Typed Polymorphic Label-Selective lambda-Calculus.
• Bard Bloom,CHOCOLATE: Calculi of Higher Order COmmunication and LAmbda TErms.
• Daniel Weise,Roger F. Crew,Michael D. Ernst,Bjarne Steensgaard,Value Dependence Graphs: Representation without Taxation.
• Hans-Juergen Boehm,Bernard Lang,Daniel M. Yellin,Amer Diwan,David Tarditi,J. Eliot B. Moss,Memory Subsystem Performance of Programs Using Copying Garbage Collection.
• Norman Ramsey,Correctness of Trap-Based Breakpoint Implementations.
• Hanne Riis Nielson,Flemming Nielson,Higher-Order Concurrent Programs with Finite Communication Topology.
• Lawrence Feigen,David Klappholz,Robert Casazza,Xing Xue,The Revival Transformation.
• Dinesh Katiyar,David C. Luckham,John C. Mitchell,A Type System for Prototyping Languages.
• Hiralal Agrawal,Dominators, Super Blocks, and Program Coverage.
• Todd A. Proebsting,Christopher W. Fraser,Detecting Pipeline Structural Hazards Quickly.
• G. Ramalingam,Thomas W. Reps,An Incremental Algorithm for Maintaining the Dominator Tree of a Reducible Flowgraph.
• Zhenyu Qian,Higher-Order Equational Logic Programming.
• Giuseppe Castagna,Benjamin C. Pierce,Decidable Bounded Quantification.
• Guy L. Steele Jr.,Building Interpreters by Composing Monads.
• Kohei Honda,Nobuko Yoshida,Combinatory Representation of Mobile Processes.

1993

• Ali-Reza Adl-Tabatabai,Thomas R. Gross,Evicted Variables and the Interaction of Global Register Allocation and Symbolic Debugging.
• Tobias Nipkow,Christian Prehofer,Type Checking Type Classes.
• Nils Klarlund,Michael I. Schwartzbach,Graph Types.
• Kim Marriott,Peter J. Stuckey,The 3 R's of Optimizing Constraint Logic Programs: Refinement, Removal and Reordering.
• Stephen Weeks,Matthias Felleisen,On the Orthogonality of Assignments and Procedures in Algol.
• Xavier Leroy,Polymorphism by Name for References and Continuations.
• Dexter Kozen,Jens Palsberg,Michael I. Schwartzbach,Efficient Recursive Subtyping.
• Damien Doligez,Xavier Leroy,A Concurrent, Generational Garbage Collector for a Multithreaded Implementation of ML.
• Qi Ning,Guang R. Gao,A Novel Framework of Register Allocation for Software Pipelining.
• Kwangkeun Yi,Williams Ludwell Harrison III,Automatic Generation and Management of Interprocedural Program Analyses.
• Shinn-Der Lee,Daniel P. Friedman,Quasi-Static Scoping: Sharing Variable Bindings Across Multiple Lexical Scopes.
• Annalisa Bossi,Michele Bugliesi,Maurizio Gabbrielli,Giorgio Levi,Maria Chiara Meo,Differential Logic Programming.
• Benjamin C. Pierce,David N. Turner,Object-Oriented Programming without Recursive Types.
• John Launchbury,A Natural Semantics for Lazy Evaluation.
• Arun Lakhotia,Constructing Call Multigraphs Using Dependence Graphs.
• Martin Odersky,Dan Rabin,Paul Hudak,Call by Name, Assignment, and the Lambda Calculus.
• Dror E. Maydan,Saman P. Amarasinghe,Monica S. Lam,Array Data-Flow Analysis and its Use in Array Privatization.
• Robert Harper,Mark Lillibridge,Explicit Polymorphism and CPS Conversion.
• G. Berry,S. Ramesh,R. K. Shyamasundar,Communicating Reactive Processes.
• Dhananjay M. Dhamdhere,Uday P. Khedker,Complexity of Bidirectional Data Flow Analysis.
• Zhong Shao,Andrew W. Appel,Smartest Recompilation.
• Siddhartha Chatterjee,John R. Gilbert,Robert Schreiber,Shang-Hua Teng,Automatic Array Alignment in Data-Parallel Programs.
• Simon L. Peyton Jones,Philip Wadler,Imperative Functional Programming.
• Jon G. Riecke,Ramesh Subrahmanyam,Algebraic Reasoning and Completeness in Typed Languages.
• Peter W. O'Hearn,Robert D. Tennent,Relational Parametricity and Local Variables.
• Daniel Leivant,Stratified Functional Programs and Computational Complexity.
• Simon J. Gay,A Sort Inference Algorithm for the Polyadic Pi-Calculus.
• Samual Bates,Susan Horwitz,Incremental Program Testing Using Program Dependence Graphs.
• Harini Srinivasan,James Hook,Michael Wolfe,Static Single Assignment for Explicitely Parallel Programs.
• Mitchell Wand,Specifying the Correctness of Binding-Time Analysis.
• Kim B. Bruce,Safe Type Checking in a Statically-Typed Object-Oriented Programming Language.
• Atsushi Ohori,Kazuhiko Kato,Semantics for Communication Primitives in an Polymorphic Language.
• Harry G. Mairson,A Constructive Logic of Multiple Subtyping.
• Martín Abadi,Luca Cardelli,Pierre-Louis Curien,Formal Parametric Polymorphism.
• Michael Codish,Saumya K. Debray,Roberto Giacobazzi,Compositional Analysis of Modular Logic Programs.
• Jong-Deok Choi,Michael G. Burke,Paul R. Carini,Efficient Flow-Sensitive Interprocedural Computation of Pointer-Induced Aliases and Side Effects.
• Maria-Virginia Aponte,Extending Record Typing to Type Parametric Modules with Sharing.
• Eric Villemonte de la Clergerie,Layer Sharing: An Improved Structure-Sharing Framework.
• Julia L. Lawall,Olivier Danvy,Separating Stages in the Continuation-Passing Style Transformation.

1992

• Jyh-Herng Chow,Williams Ludwell Harrison III,Compile-Time Analysis of Parallel Programs that Share Memory.
• Dave Berry,Robin Milner,David N. Turner,A Semantics for ML Concurrency Primitives.
• Roberto Di Cosmo,Type Isomorphisms in a Type-Assignment Framework.
• Daniel R. Edelson,A Mark-and-Sweep Collector for C++.
• Patrick Cousot,Radhia Cousot,Inductive Definitions, Semantics and Abstract Interpretation.
• Hanne Riis Nielson,Flemming Nielson,Bounded Fixed Point Iteration.
• Ravi Sethi,Philip Wadler,The Essence of Functional Programming.
• Kim B. Bruce,John C. Mitchell,PER Models of Subtyping, Recursive Types and Higher-Order Polymorphism.
• Robert Cartwright,Matthias Felleisen,Observable Sequentiality and Full Abstraction.
• Benjamin C. Pierce,Bounded Quantification is Undecidable.
• QingMing Ma,Parametricity as Subtyping.
• Patrick Lincoln,John C. Mitchell,Algorithmic Aspects of Type Inference with Subtypes.
• Yuh-Jzer Joung,Scott A. Smolka,A Comprehensive Study of the Complexity of Multiparty Interaction.
• Mads Tofte,Principal Signatures for Higher-Order Program Modules.
• Thomas Ball,James R. Larus,Optimally Profiling and Tracing Programs.
• Charles Farnum,Pattern-Based Tree Attribution.
• Edmund M. Clarke,Orna Grumberg,David E. Long,Model Checking and Abstraction.
• Atsushi Ohori,A Compilation Method for ML-Style Polymorphic Record Calculi.
• Andrzej Filinski,Linear Continuations.
• Didier Rémy,Typing Record Concatenation for Free.
• Rodney Farrow,Thomas J. Marlowe,Daniel M. Yellin,Composable Attribute Grammars: Support for Modularity in Translator Design and Implementation.
• Vivek Nirkhe,William Pugh,Partial Evaluation of High-Level Imperative Programming Languages, with Applications in Hard Real-Time Systems.
• Georges Gonthier,Martín Abadi,Jean-Jacques Lévy,The Geometry of Optimal Lambda Reduction.
• Bernard Lang,Christian Queinnec,José M. Piquer,Garbage Collecting the World.
• Radha Jagadeesan,Keshav Pingali,Abstract Semantics for a Higher-Order Functional Language with Logic Variables.
• Martin C. Rinard,Monica S. Lam,Semantic Foundations of Jade.
• Jesper Jørgensen,Generating a Compiler for a Lazy Language by Partial Evaluation.
• Rajiv Gupta,Generalized Dominators and Post-Dominators.
• Xavier Leroy,Unboxed Objects and Polymorphic Typing.
• Roberto Barbuti,Michael Codish,Roberto Giacobazzi,Giorgio Levi,Modeling Prolog Control.
• Joseph Bates,Alon Lavie,Recognizing Substrings of LR(k) Languages in Linear Time.

1991

• Yuh-Jzer Joung,Scott A. Smolka,Coordinating First-Order Multiparty Interactions.
• Robert Harper,Benjamin C. Pierce,A Record Calculus Based on Symmetric Concatenation.
• John C. Mitchell,Sigurd Meldal,Neel Madhav,An Extension of Standard ML Modules with Subtyping and Inheritance.
• Roberto M. Amadio,Luca Cardelli,Subtyping Recursive Types.
• Erik Crank,Matthias Felleisen,Parameter-Passing and the Lambda Calculus.
• David S. Wise,R. S. Sundaresh,Paul Hudak,Incremental Compilation via Partial Evaluation.
• Dorai Sitaram,Matthias Felleisen,Modeling Continuations without Continuations.
• Fritz Henglein,Harry G. Mairson,The Complexity of Type Inference for Higher-Order Typed Lambda Calculi.
• Vijay A. Saraswat,Martin C. Rinard,Prakash Panangaden,Semantic Foundations of Concurrent Constraint Programming.
• Jon G. Riecke,Fully Abstract Translations between Functional Languages.
• Shlomit S. Pinter,Ron Y. Pinter,Program Optimization and Parallelization Using Idioms.
• Bruce F. Duba,Robert Harper,David B. MacQueen,Typing First-Class Continuations in ML.
• William Landi,Barbara G. Ryder,Pointer-Induced Aliasing: A Problem Classification.
• Keshav Pingali,Micah Beck,Richard Johnson,Mayan Moudgill,Paul Stodghill,Dependence Flow Graphs: An Algebraic Approach to Program Dependencies.
• Vaughan R. Pratt,Modeling Concurrency with Geometry.
• Jong-Deok Choi,Ron Cytron,Jeanne Ferrante,Automatic Construction of Sparse Data Flow Evaluation Graphs.
• Martín Abadi,Gordon D. Plotkin,A Logical View of Composition and Refinement.
• R. C. Sekar,Prateek Mishra,I. V. Ramakrishnan,On the Power and Limitation of Strictness Analysis Based on Abstract Interpretation.
• Steven Lucco,Oliver Sharp,Parallel Programming With Coordination Structures.
• Jiazhen Cai,Robert Paige,``Look Ma, No Hashing, And No Arrays Neither''.
• Martin Odersky,How to Make Destructive Updates Less Destructive.
• William D. Clinger,Jonathan Rees,Macros That Work.
• Alon Kleinman,Yael Moscowitz,Amir Pnueli,Ehud Y. Shapiro,Communication with Directed Logic Variables.
• Thomas A. Henzinger,Zohar Manna,Amir Pnueli,Temporal Proof Methodologies for Real-time Systems.
• Charles Consel,Olivier Danvy,Static and Dynamic Semantics Processing.
• Samson Abramsky,Thomas P. Jensen,A Relational Approach to Strictness Analysis for Higher-Order Polymorphic Functions.
• Xavier Leroy,Pierre Weis,Polymorphic Type Inference and Assignment.
• Christian Queinnec,Bernard P. Serpette,A Dynamic Extent Control Operator for Partial Continuations.
• Alexander Aiken,Brian R. Murphy,Static Type Inference in a Dynamically Typed Language.
• Luc Maranget,Optimal Derivations in Weak Lambda-calculi and in Orthogonal Terms Rewriting Systems.
• Pierre Jouvelot,David K. Gifford,Algebraic Reconstruction of Types and Effects.

1990

• John C. Mitchell,Toward a Typed Foundation for Method Specialization and Inheritance.
• Paul C. Attie,Nissim Francez,Orna Grumberg,Fairness and Hyperfairness in Multi-Party Interactions.
• François Rouaix,Safe Run-time Overloading.
• William R. Cook,Walter L. Hill,Peter S. Canning,Inheritance Is Not Subtyping.
• Frances E. Allen,John Field,On Laziness and Optimality in Lambda Interpreters: Tools for Specification and Analysis.
• Andrea Asperti,Gian Luigi Ferrari,Roberto Gorrieri,Implicative Formulae in the ``Proofs as Computations'' Analogy.
• Timothy Griffin,A Formulae-as-Types Notion of Control.
• Vijay A. Saraswat,Martin C. Rinard,Concurrent Constraint Programming.
• Nevin Heintze,Joxan Jaffar,A Finite Presentation Theorem for Approximating Logic Programs.
• R. C. Sekar,Shaunak Pawagi,I. V. Ramakrishnan,Small Domains Spell Fast Strictness Analysis.
• John Lamping,An Algorithm for Optimal Lambda Calculus Reduction.
• Alexander Aiken,John H. Williams,Edward L. Wimmers,Program Transformation in the Presence of Errors.
• Robert Harper,John C. Mitchell,Eugenio Moggi,Higher-Order Modules and the Phase Distinction.
• Yiannis N. Moschovakis,Computable processes.
• Alan J. Demers,Mark Weiser,Barry Hayes,Hans-Juergen Boehm,Daniel G. Bobrow,Scott Shenker,Combining Generational and Conservative Garbage Collection: Framework and Implementations.
• Satish R. Thatte,Quasi-Static Typing.
• Thomas J. Marlowe,Barbara G. Ryder,An Efficient Hybrid Algorithm for Incremental Data Flow Analysis.
• Martín Abadi,Luca Cardelli,Pierre-Louis Curien,Jean-Jacques Lévy,Explicit Substitutions.
• Guy L. Steele Jr.,Making Asynchronous Parallelism Safe for the World.
• R. Ramesh,I. V. Ramakrishnan,David Scott Warren,Automata-Driven Indexing of Prolog Clauses.
• Carl A. Gunter,Relating Total and Partial Correctness Interpretations of Non-Deterministic Programs.
• Yves Lafont,Interaction Nets.
• Justin O. Graver,Ralph E. Johnson,A Type System for Smalltalk.
• Krishna V. Palem,Barbara B. Simons,Scheduling Time-Critical Instructions on RISC Machines.
• Geoffrey L. Burn,A Relationship Between Abstract Interpretation and Projection Analysis.
• Raghu Ramakrishnan,Parallelism in Logic Programs.
• Eugene W. Stark,On the Relations Computable by a Class of Concurrent Automata.
• Alain Deutsch,On Determining Lifetime and Aliasing of Dynamically Allocated Data in Higher-Order Functional Specifications.
• Harry G. Mairson,Deciding ML Typability is Complete for Deterministic Exponential Time.
• James R. Russell,On Oraclizable Networks and Kahn's Principle.
• Gérard Berry,Gérard Boudol,The Chemical Abstract Machine.

1989

• Katherine A. Yelick,Joseph L. Zachary,Moded Type Systems for Logic Programming.
• Paul C. Attie,E. Allen Emerson,Synthesis of Concurrent Systems with Many Similar Sequential Processes.
• Marianne Baudinet,Temporal Logic Programming is Complete and Expressive.
• William Baxter,Henry R. Bauer III,The Program Dependence Graph and Vectorization.
• Christine Paulin-Mohring,Extracting F(omega)'s Programs from Proofs in the Calculus of Constructions.
• Bent Thomsen,A Calculus of Higher Order Communicating Systems.
• Andrew W. Appel,Trevor Jim,Continuation-Passing, Closure-Passing Style.
• Kim Guldstrand Larsen,Arne Skou,Bisimulation Through Probabilistic Testing.
• Bengt Jonsson,A Fully Abstract Trace Model for Dataflow Networks.
• Ron Cytron,Jeanne Ferrante,Barry K. Rosen,Mark N. Wegman,F. Kenneth Zadeck,An Efficient Method of Computing Static Single Assignment Form.
• E. Allen Emerson,Tom Sadler,Jai Srinivasan,Efficient Temporal Reasoning.
• Haim Gaifman,Ehud Y. Shapiro,Fully Abstract Compositional Semantics for Logic Programs.
• Timothy J. Hickey,CLP* and Constraint Abstraction.
• Luca Cardelli,James E. Donahue,Mick J. Jordan,Bill Kalsow,Greg Nelson,The Modula-3 Type System.
• Nachum Dershowitz,Stéphane Kaplan,Rewrite, Rewrite, Rewrite, Rewrite, Rewrite.
• Peter D. Mosses,Unified Algebras and Modules.
• Richard Kelsey,Paul Hudak,Realistic Compilation by Program Transformation.
• Keith D. Cooper,Ken Kennedy,Fast Interprocedural Alias Analysis.
• Paris C. Kanellakis,John C. Mitchell,Polymorphic Unification and ML Typing.
• William Pugh,Tim Teitelbaum,Incremental Computation via Function Caching.
• Gennaro Monteleone,Generalized Conjunctive Types.
• José Meseguer,Relating Models of Polymorphism.
• Shmuel Sagiv,O. Edelstein,Nissim Francez,Michael Rodeh,Resolving Circularity in Attribute Grammars with Applications to Data Flow Analysis.
• Martín Abadi,Luca Cardelli,Benjamin C. Pierce,Gordon D. Plotkin,Dynamic Typing in a Statically-Typed Language.
• Rebecca Parsons Selke,A Rewriting Semantics for Program Dependence Graphs.
• Amir Pnueli,Roni Rosner,On the Synthesis of a Reactive Module.
• Philip Wadler,Stephen Blott,How to Make ad-hoc Polymorphism Less ad-hoc.
• Douglas Stott Parker Jr.,Partial Order Programming.
• Didier Rémy,Typechecking Records and Variants in a Natural Extension of ML.
• K. Gopinath,John L. Hennessy,Copy Elimination in Functional Languages.

1988

• Philip Wadler,Strictness Analysis Aids Time Analysis.
• Gregory F. Johnson,Dominic Duggan,Stores and Partial Continuations as First-Class Objects in a Language and its Environment.
• Ryan Stansifer,Type Inference with Subtypes.
• Matthias Felleisen,The Theory and Practice of First-Class Prompts.
• Margaret Montenyohl,Mitchell Wand,Correct Flow Analysis in Continuation Semantics.
• Martin D. Carroll,Barbara G. Ryder,Incremental Data Flow Analysis via Dominator and Attribute Updates.
• Albert R. Meyer,Kurt Sieber,Towards Fully Abstract Semantics for Local Variables.
• Paul Hudak,Jonathan Young,A Collecting Interpretation of Expressions (Without Powerdomains).
• Bard Bloom,Sorin Istrail,Albert R. Meyer,Bisimulation Can't Be Traced.
• Jeanne Ferrante,P. Mager,Bowen Alpern,Mark N. Wegman,F. Kenneth Zadeck,Detecting Equality of Variables in Programs.
• Luca Cardelli,Structural Subtyping and the Notion of Power Type.
• Saumya K. Debray,Efficient Dataflow Analysis of Logic Programs.
• Cristina Ruggieri,Thomas P. Murtagh,Lifetime Analysis of Dynamically Allocated Objects.
• Susan Horwitz,Jan Prins,Thomas W. Reps,On the Adequacy of Program Dependence Graphs for Representing Programs.
• Barry K. Rosen,Mark N. Wegman,F. Kenneth Zadeck,Global Value Numbers and Redundant Computations.
• Eduardo Pelegrí-Llopart,Susan L. Graham,Optimal Code Generation for Expression Trees: An Application of BURS Theory.
• John H. Williams,Edward L. Wimmers,Sacrificing Simplicity for Convenience: Where Do You Draw the Line?
• Moshe Y. Vardi,A Temporal Fixpoint Calculus.
• Stephen J. Garland,John V. Guttag,Inductive Methods for Reasoning about Abstract Data Types.
• Susan Horwitz,Jan Prins,Thomas W. Reps,Integrating Non-Interfering Versions of Programs.
• John M. Lucassen,David K. Gifford,Polymorphic Effect Systems.
• Monica S. Lam,Compiler Optimizations for Asynchronous Systolic Array Programs.
• A. J. Kfoury,Jerzy Tiuryn,Pawel Urzyczyn,A Proper Extension of ML with an Effective Type-Assignment.
• Hanne Riis Nielson,Flemming Nielson,Automatic Binding Time Analysis for a Typed Lambda-Calculus.
• François Irigoin,Rémi Triolet,Supernode Partitioning.
• Luc Bougé,Nissim Francez,A Compositional Approach to Superimposition.
• John C. Mitchell,Robert Harper,The Essence of ML.
• Samuel N. Kamin,Inheritance in Smalltalk-80: A Denotational Definition.

1987

• Peter Lee,Uwe F. Pleban,A Realistic Compiler Generator Based on High-Level Semantics.
• Zohar Manna,Amir Pnueli,Specification and Verification of Concurrent Programs By Forall-Automata.
• Philip Wadler,Views: A Way for Pattern Matching to Cohabit with Data Abstraction.
• Frank J. Oles,Semantics for Concurrency without Powerdomains.
• Daniel Leivant,Tim Fernando,Skinny and Fleshy Failures of Relative Completeness.
• Vijay A. Saraswat,The Concurrent Logic Programming Language CP: Definition and Operational Semantics.
• Jennifer Widom,David Gries,Fred B. Schneider,Completeness and Incompleteness of Trace-Based Network Proof Systems.
• Anne Neirynck,Prakash Panangaden,Alan J. Demers,Computation of Aliases and Support Sets.
• Flemming Nielson,Strictness Analysis and Denotational Abstract Interpretation.
• Cordelia V. Hall,David S. Wise,Compiling Strictness into Streams.
• David Gelernter,Suresh Jagannathan,Thomas London,Environments as First Class Objects.
• M. Drew Moshier,William C. Rounds,A Logic for Partially Specified Data Structures.
• Jiazhen Cai,Robert Paige,Binding Performance at Language Design Time.
• Randy Allen,David Callahan,Ken Kennedy,Automatic Decomposition of Scientific Programs for Parallel Execution.
• Krzysztof R. Apt,Nissim Francez,Shmuel Katz,Appraising Fairness in Languages for Distributed Programming.
• Maurice Herlihy,Jeannette M. Wing,Axioms for Concurrent Objects.
• David R. Cheriton,Michael E. Wolf,Extensions for Multi-Module Records in Conventional Programming Languages.
• Eugene W. Stark,Concurrent Transition System Semantics of Process Networks.
• Cornelis Huizing,Rob Gerth,Willem P. de Roever,Full Abstraction of a Real-Time Denotational Semantics for an Occam-like Language.
• David Bernstein,Jeffrey M. Jaffe,Michael Rodeh,Scheduling Arithmetic and Load Operations in Parallel with No Spilling.
• Paul Caspi,Daniel Pilaud,Nicolas Halbwachs,John Plaice,Lustre: A Declarative Language for Programming Synchronous Systems.
• Albert R. Meyer,John C. Mitchell,Eugenio Moggi,Richard Statman,Empty Types in Polymorphic Lambda Calculus.
• Pierre Jouvelot,Semantic Parallelization: A Practical Exercise in Abstract Interpretation.
• Matthias Felleisen,Daniel P. Friedman,A Calculus for Assignments in Higher-Order Languages.
• Val Tannen,Albert R. Meyer,Computable Values Can Be Classical.
• David R. Chase,An Improvement to Bottom-up Tree Pattern Matching.
• Joxan Jaffar,Jean-Louis Lassez,Constraint Logic Programming.
• Tsung-Min Kuo,Prateek Mishra,On Strictness and its Analysis.
• Eugene E. Kohlbecker,Mitchell Wand,Macro-by-Example: Deriving Syntactic Transformations from their Specifications.

1986

• Deborah S. Coutant,Retargetable High-Level Alias Analysis.
• David B. MacQueen,Using Dependent Types to Express Modular Structure.
• Hassan Aït-Kaci,Roger Nasr,Logic and Inheritance.
• Mitchell Wand,Finding the Source of Type Errors.
• Howard Barringer,Ruurd Kuiper,Amir Pnueli,A Really Abstract Concurrent Model and its Temporal Logic.
• Takuya Katayama,Hisashi Sasaki,Global Storage Allocation in Attribute Evaluation.
• Reino Kurki-Suonio,Towards Programming with Knowledge Expressions.
• Paul Hudak,Jonathan Young,Higher-Order Strictness Analysis in Untyped Lambda Calculus.
• Neil D. Jones,Alan Mycroft,Data Flow Analysis of Applicative Programs Using Minimal Function Graphs.
• Raghu Ramakrishnan,Abraham Silberschatz,Annotations for Distributed Programming in Logic.
• Stan Jefferson,Samuel N. Kamin,Executable Specifications with Quantifiers in the FASE System.
• John C. Mitchell,Representation Independence and Data Abstraction.
• Gregor Snelting,Wolfgang Henhapl,Unification in Many-Sorted Algebras as a Device for Incremental Semantic Analysis.
• Philip J. Hatcher,Thomas W. Christopher,High-Quality Code Generation Via Bottom-Up Tree Pattern Matching.
• Barbara Liskov,Maurice Herlihy,Lucy Gilbert,Limitations of Synchronous Communication with Static Process Structure in Languages for Distributed Computing.
• Paul Hudak,Lauren Smith,Para-Functional Programming: A Paradigm for Programming Multiprocessor Systems.
• Pierre Wolper,Expressing Interesting Properties of Programs in Propositional Temporal Logic.
• Thomas W. Reps,Carla Marceau,Tim Teitelbaum,Remote Attribute Updating for Language-Based Editors.
• Ron Cytron,Andy Lowry,F. Kenneth Zadeck,Code Motion of Control Structures in High-Level Languages.
• Ulrik Jørring,William L. Scherlis,Compilers and Staging Transformations.
• Albert R. Meyer,Mark B. Reinhold,``Type'' Is Not A Type.
• Nicholas Carriero,David Gelernter,Jerrold Leichter,Distributed Data Structures in Linda.
• Irene Greif,Robert Seliger,William E. Weihl,Atomic Data Abstractions in a Distributed Collaborative Editing System.
• Marina C. Chen,A Parallel Language and its Compilation to Multiprocessor Machines or VLSI.
• Larry G. Jones,Janos Simon,Hierarchical VLSI Design Systems Based on Attribute Grammars.
• Jia-Huai You,P. A. Subrahmanyam,Equational Logic Programming: An Extension to Equational Programming.
• Gregory F. Johnson,Janet A. Walz,A Maximum-Flow Approach to Anomaly Isolation in Unification-Based Incremental Type Inference.
• Pierre America,Jaco de Bakker,Joost N. Kok,Jan J. M. M. Rutten,Operational Semantics of a Parallel Object-Oriented Language.
• Christian Lengauer,Chua-Huang Huang,A Mechanically Certified Theorem about Optimal Concurrency of Sorting Networks.
• Roger Hoover,Dynamically Bypassing Copy Rule Chains in Attribute Grammars.

1985

• Robert Cartwright,Types as Intervals.
• Van Nguyen,David Gries,Susan S. Owicki,A Model and Temporal Proof System for Networks of Processes.
• Leslie Lamport,What It Means for a Concurrent Program to Satisfy a Specification: Why No One Has Specified Priority.
• Daniel P. Friedman,Christopher T. Haynes,Constraining Control.
• Gary Lindstrom,Functional Programming and the Logical Variable.
• Ray Ford,Duangkaew Sawamiphakdi,A Greedy Approach to Incremental Code Generation.
• Gregory F. Johnson,Charles N. Fischer,A Meta-Language and System for Nonlocal Incremental Attribute Evaluation in Language-Based Editors.
• E. Allen Emerson,Chin-Laung Lei,Modalities for Model Checking: Branching Time Strikes Back.
• Andrew W. Appel,Semantics-Directed Code Generation.
• Mary S. Van Deusen,Zvi Galil,Brian K. Reid,Mitchell Wand,Embedding Type Structure in Semantics.
• Daniel Leivant,Logical and Mathematical Reasoning about Imperative Programs.
• Mark N. Wegman,F. Kenneth Zadeck,Constant Propagation with Conditional Branches.
• Michael B. Jones,Richard F. Rashid,Mary R. Thompson,Matchmaker: An Interface Specification Language for Distributed Processing.
• Julian A. Padget,John P. Fitch,Closurize and Concentrate.
• Jeanne Ferrante,Mary Mace,On Linearizing Parallel Code.
• Paul Hudak,Adrienne G. Bloss,The Aggregate Update Problem in Functional Programming Systems.
• Thomas S. Anantharaman,Edmund M. Clarke,Michael J. Foster,Bud Mishra,Compiling Path Expressions into VLSI Circuits.
• David Bernstein,Ron Y. Pinter,Michael Rodeh,Optimal Scheduling of Arithmetic Operations in Parallel with Memory Accesses.
• Orna Lichtenstein,Amir Pnueli,Checking That Finite State Concurrent Programs Satisfy Their Linear Specification.
• Christopher W. Fraser,David R. Hanson,High-Level Language Facilities for Low-Level Services.
• Donald Sannella,Andrzej Tarlecki,Program Specification and Development in Standard ML.
• Prateek Mishra,Uday S. Reddy,Declaration-Free Type Checking.
• Joseph Y. Halpern,John H. Williams,Edward L. Wimmers,Timothy C. Winkler,Denotational Semantics and Rewrite Rules for FP.
• John C. Mitchell,Gordon D. Plotkin,Abstract Types Have Existential Type.
• Leslie Lamport,Fred B. Schneider,Constraints: A Uniform Approach to Aliasing and Typing.
• Lori L. Pollock,Mary Lou Soffa,Incremental Compilation of Locally Optimized Code.
• Alfred V. Aho,Mahadevan Ganapathi,Efficient Tree Pattern Matching: An Aid to Code Generation.
• Walter F. Tichy,Mark C. Baker,Smart Recompilation.
• Keith D. Cooper,Analyzing Aliases of Reference Formal Parameters.
• Kokichi Futatsugi,Joseph A. Goguen,Jean-Pierre Jouannaud,José Meseguer,Principles of OBJ2.

1984

• Ken Kennedy,Mary S. Van Deusen,Larry Landweber,Richard C. Waters,Expressional Loops.
• P. A. Subrahmanyam,Jia-Huai You,Pattern Driven Lazy Reduction: A Unifying Evaluation Mechanism for Functional and Logic Programs.
• Steven D. Johnson,Applicative Programming and Digital Design.
• Jerald S. Schwarz,Dean Rubine,Treat - An Applicative Code Generator.
• Mark Sherman,Paragon: Novel Uses of Type Hierarchies for Data Abstraction.
• Dennis Shasha,Amir Pnueli,W. Ewald,Temporal Verification of Carrier-Sense Local Area Network Protocols.
• Joe D. Warren,A Hierarchical Basis for Reordering Transformations.
• David B. MacQueen,Gordon D. Plotkin,Ravi Sethi,An Ideal Model for Recursive Polymorphic Types.
• Harold Ossher,Grids: A New Program Structuring Mechanism Based on Layered Graphs.
• Joseph Y. Halpern,Albert R. Meyer,Boris A. Trakhtenbrot,The Semantics of Local Storage, or What Makes the Free-List Free?
• Norihisa Suzuki,Minoru Terada,Creating Efficient Systems for Object-Oriented Languages.
• Prateek Mishra,Robert M. Keller,Static Inference of Properties of Applicative Programs.
• Brian Cantwell Smith,Reflection and Semantics in Lisp.
• Jean-Claude Raoult,Ravi Sethi,The Global Storage Needs of a Subcomputation.
• Ehud Y. Shapiro,Systems Programming in Concurrent Prolog.
• L. Peter Deutsch,Allan M. Schiffman,Efficient Implementation of the Smalltalk-80 System.
• Robert G. Bandes,Constraining-Unification and the Programming Language Unicorn.
• Paul Hudak,David A. Kranz,A Combinator-Based Compiler for a Functional Language.
• John C. Mitchell,Coercion and Type Inference.
• Michal Grabowski,On Relative Completeness of Programming Logics.
• Christoph M. Hoffmann,Michael J. O'Donnell,Implementation of an Interpreter for Abstract Equations.
• Eugene W. Myers,Efficient Applicative Data Types.
• Jean-Pierre Jouannaud,Hélène Kirchner,Completion of a Set of Rules Modulo a Set of Equations.
• Joseph Y. Halpern,A Good Hoare Axiom System for an Algol-like Language.
• Robert P. Nix,Editing by Example.
• Thomas P. Murtagh,A Less Dynamic Memory Allocation Scheme for Algol-like Languages.
• Thomas W. Reps,Bowen Alpern,Interactive Proof Checking.
• Don Milos,Uwe F. Pleban,George Loegel,Direct Implementation of Compiler Specifications or the Pascal P-code Compiler Revisited.
• Reinhard Wilhelm,Inverse Currying Transformation on Attribute Grammars.
• Mitchell Wand,A Types-as-Sets Semantics for Milner-Style Polymorphism.
• Jean-Jacques Thiel,Stop Losing Sleep Over Incomplete Data Type Specifications.
• Nissim Francez,Dexter Kozen,Generalized Fair Termination.

1983

• John R. Allen,Ken Kennedy,Carrie Porterfield,Joe D. Warren,Conversion of Control Dependence to Data Dependence.
• Daniel Leivant,Polymorphic Type Inference.
• Barbara G. Ryder,Incremental Data Flow Analysis.
• Bent Bruun Kristensen,Ole Lehrmann Madsen,Birger Møller-Pedersen,Kristen Nygaard,Abstraction Mechanisms in the Beta Programming Language.
• Mitchell Wand,Loops in Combinator-Based Compilers.
• Lambert G. L. T. Meertens,Incremental Polymorphic Type Checking in B.
• John Nagle,Scott Johnson,Practical Program Verification: Automatic Program Proving for Real-Time Embedded Software.
• Richard B. Kieburtz,Precise Typing of Abstract Data Type Specifications.
• Zohar Manna,Amir Pnueli,How to Cook a Temporal Proof System for Your Pet Language.
• Robert E. Strom,Mechanisms for Compile-Time Enforcement of Security.
• Naftaly H. Minsky,Locality in Software Systems.
• Ralph-Johan Back,Heikki Mannila,Kari-Jouko Räihä,Derivation of Efficient DAG Marking Algorithms.
• Alan J. Demers,James E. Donahue,Making Variables Abstract: An Equational Theory for Russell.
• Jeffrey Bonar,Elliot Soloway,Uncovering Principles of Novice Programming.
• Pierre Lescanne,Computer Experiments with the Reve Term Rewriting System Generator.
• Robert Paige,Transformational Programming - Applications to Algorithms and Systems.
• John R. Wright,Larry Landweber,Alan J. Demers,Tim Teitelbaum,Vaughan R. Pratt,Five Paradigm Shifts in Language Design and their Realization in Viron, a Dataflow Programming Environment.
• Edmund M. Clarke,E. Allen Emerson,A. Prasad Sistla,Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach.
• Mark N. Wegman,Summarizing Graphs by Regular Expressions.
• Daniel Leivant,Structural Semantics for Polymorphic Data Types.
• Butler W. Lampson,Eric E. Schmidt,Practical Use of a Polymorphic Applicative Language.
• Janice E. Cuny,Lawrence Snyder,Compilation of Data-Driven Programs for Synchronous Execution.
• E. Allen Emerson,Joseph Y. Halpern,``Sometimes'' and ``Not Never'' Revisited: On Branching Versus Linear Time.
• Jeanne Ferrante,Karl J. Ottenstein,A Program Form Based on Data Dependency in Predicate Regions.
• Peter Wegner,On the Unification of Data and Program Abstraction in Ada.
• Stephen C. Johnson,Code Generation for Silicon.
• Greg Nelson,Verifying Reachability Invariants of Linked Structures.
• Leslie Lamport,Reasoning About Nonatomic Operations.

1982

• Robert Giegerich,Automatic Generation of Machine Specific Code Optimizers.
• Barbara Liskov,Robert Scheifler,Guardians and Actions: Linguistic Support for Robust, Distributed Programs.
• Edmund M. Clarke,Steven M. German,Joseph Y. Halpern,On Effective Axiomatizations of Hoare Logics.
• John L. Hennessy,Thomas R. Gross,Code Generation and Reorganization in the Presence of Pipeline Constraints.
• Neil D. Jones,Steven S. Muchnick,A Flexible Approach to Interprocedural Data Flow Analysis and Programs with Recursive Data Structures.
• Richard A. DeMillo,Sergiu Hart,Micha Sharir,Amir Pnueli,Termination of Probabilistic Concurrent Programs.
• Erik Sandewall,Unified Dialogue Management in the Carousel System.
• Lawrence C. Paulson,A Semantics-Directed Compiler Generator.
• Albert R. Meyer,John C. Mitchell,Axiomatic Definability and Completeness for Recursive Programs.
• Rivi Sherman,Amir Pnueli,David Harel,Is the Interesting Part of Process Logic Uninteresting - A Translation from PL to PDL.
• Martin C. Henson,Raymond Turner,Completion Semantics, Interpreter Generation.
• Gregory F. Johnson,Charles N. Fischer,Non-Syntactic Attribute Flow in Language Based Editors.
• Mitchell Wand,Semantics-Directed Machine Architecture.
• Vaughan R. Pratt,On the Composition of Processes.
• David W. Wall,Messages as Active Agents.
• Henryk Jan Komorowski,Partial Evaluation as a Means for Inferencing Data Structures in an Applicative Language: A Theory and Implementation in the Case of Prolog.
• Eric C. Cooper,On the Expressive Power of Query Languages for Relational Databases.
• Brent Hailpern,Susan S. Owicki,Modular Verification of Concurrent Programs.
• Nissim Francez,Extended Naming Conventions for Communicating Processes.
• John H. Reif,Paul G. Spirakis,Unbounded Speed Variability in Distributed Communication Systems.
• Pierre Wolper,Specification and Synthesis of Communicating Processes using an Extended Temporal Logic.
• M. V. S. Ramanath,Marvin H. Solomon,Optimal Code for Control Structures.
• Richard J. Lipton,Robert Sedgewick,Jacobo Valdes,Programming Aspects of VLSI.
• Mahadevan Ganapathi,Charles N. Fischer,Description-Driven Code Generation using Attribute Grammars.
• Ehud Y. Shapiro,Algorithmic Program Diagnosis.
• E. Gansner,Joseph R. Horgan,Chandra M. R. Kintala,D. J. Moore,P. Surko,Semantics and Correctness of a Query Language Translation.
• Seppo Sippu,Eljas Soisalon-Soininen,Practical Error Recovery in LR Parsing.
• Adrienne Critcher,On the Ability of Structures to Store and Access Information.
• Jack W. Davidson,Christopher W. Fraser,Eliminating Redundant Object Code.
• David Sandberg,Lithe: A Language Combining a Flexible Syntax, Classes.
• Thomas W. Reps,Optimal-Time Incremental Semantic Analysis for Syntax-Directed Editors.
• Shaula Yemini,An Axiomatic Treatment of Exception Handling.
• Luís Damas,Robin Milner,Principal Type-Schemes for Functional Programs.
• Hans-Juergen Boehm,A Logic for Expressions with Side-Effects.
• Alan Borning,Daniel H. H. Ingalls,A Type Declaration and Inference System for Smalltalk.
• Fahimeh Jalili,Jean H. Gallier,Building Friendly Parsers.
• Paul J. Voda,Maple: a Programming Language, Operating System.
• Rodney Farrow,Experience with an Attribute Grammar-Based Compiler.

1981

• Susan S. Owicki,Making the World Safe for Garbage Collection.
• John L. Hennessy,Program Optimization and Exception Handling.
• Robert Cartwright,Robert Hood,Philip Mathews,Paths: An Abstract Alternative to Pointers.
• J. Ramanathan,C. J. Shubra,Modeling of Problem Domains for Driving Program Development Systems.
• William L. Scherlis,Program Improvement by Internal Specialization.
• Norihisa Suzuki,Inferring Types in Smalltalk.
• Joseph Y. Halpern,Albert R. Meyer,Axiomatic Definitions of Programming Languages, II.
• Michael W. Condry,Paging as a ``Language Processing'' Task.
• Cyril N. Alberga,Alfred L. Brown,George B. Leeman Jr.,Martin Mikelsons,Mark N. Wegman,A Program Development Tool.
• Daniel J. Lehmann,Michael O. Rabin,On the Advantages of Free Choice: A Symmetric and Fully Distributed Solution to the Dining Philosophers Problem.
• Ashok K. Chandra,Programming Primitives for Database Languages.
• Barry K. Rosen,Linear Cost is Sometimes Quadratic.
• Vaughan R. Pratt,Program Logic Without Binding is Decidable.
• Eugene W. Myers,A Precise Interprocedural Data Flow Algorithm.
• Wolfgang Polak,Program Verification Based on Denotational Semantics.
• Robert Cartwright,Formal Program Testing.
• John White,Richard J. Lipton,Patricia C. Goldberg,P. Geoffrey Lowney,Carrier Arrays: An Idiom-Preserving Extension to APL.
• Takuya Katayama,Yutaka Hoshino,Verification of Attribute Grammars.
• Alan J. Demers,Thomas W. Reps,Tim Teitelbaum,Incremental Evaluation for Attribute Grammars with Application to Syntax-Directed Editors.
• David J. Kuck,Robert H. Kuhn,David A. Padua,Bruce Leasure,Michael Wolfe,Dependence Graphs and Compiler Optimizations.
• Mordechai Ben-Ari,Zohar Manna,Amir Pnueli,The Temporal Logic of Branching Time.

1980

• Zohar Manna,Amir Pnueli,Synchronous Schemes and Their Decision Problems.
• Dov M. Gabbay,Amir Pnueli,Saharon Shelah,Jonathan Stavi,On the Temporal Basis of Fairness.
• Vaughan R. Pratt,On Specifying Verifiers.
• Brian K. Reid,A High-Level Approach to Computer Document Formatting.
• Ravi Sethi,A Case Study in Specifying the Semantics of a Programming Language.
• Harry B. Hunt III,Daniel J. Rosenkrantz,Efficient Algorithms for Structural Similarity of Grammars.
• John V. Guttag,James J. Horning,Formal Specification as a Design Tool.
• Timothy A. Budd,Richard A. DeMillo,Richard J. Lipton,Frederick G. Sayward,Theoretical and Emperical Studies on Using Program Mutation to Test the Functional Correctness of Programs.
• Rohit Parikh,Propositional Logics of Programs: Systems, Models, and Complexity.
• David R. Musser,On Proving Inductive Properties of Abstract Data Types.
• Samuel N. Kamin,Final Data Tye Specifications: A New Data Type Specification Method.
• Robert Endre Tarjan,Prime Subprogram Parsing of a Program.
• Albert R. Meyer,Joseph Y. Halpern,Axiomatic Definitions of Programming Languages: A Theoretical Assessment.
• James H. Morris Jr.,Eric Schmidt,Philip Wadler,Experience with an Applicative String Processing Language.
• Alan J. Demers,James E. Donahue,Data Types, Parameters, and Type Checking.
• L. Howard Holley,Barry K. Rosen,Qualified Data Flow Problems.
• Alan J. Demers,James E. Donahue,``Type-Completeness'' as a Language Design Principle.
• Paul W. Abrahams,Richard J. Lipton,Stephen R. Bourne,Norihisa Suzuki,Analysis of Pointer Rotation.
• Leslie Lamport,``Sometime'' is Sometimes ``Not Never'' - On the Temporal Logic of Programs.
• Daniel P. Friedman,David S. Wise,An Indeterminate Constructor for Applicative Programming.
• Paul Klint,An Overview of the Summer Programming Language.
• A. J. Kfoury,Analysis of Simple Programs Over Different Sets of Primitives.
• John H. Reif,Gary L. Peterson,A Dynamic Logic of Multiprocessing with Incomplete Information.
• William E. Weihl,Interprocedural Data Flow Analysis in the Presence of Pointers, Procedure Variables and Label Variables.
• Deepak Kapur,Mandayam K. Srivas,Expressiveness of the Operation Set of a Data Abstraction.

1979

• Patrick Cousot,Radhia Cousot,Systematic Design of Program Analysis Frameworks.
• Robert L. Constable,Scott Johnson,A PL/CV Precis.
• Ken C. Liu,Arthur C. Fleck,String Pattern Matching in Polynomial Time.
• Robert Cartwright,John McCarthy,First Order Programming Logic.
• Adrienne Critcher,The Functional Power of Parameter Passage Mechanisms.
• W. E. Gull,Michael A. Jenkins,Decisions for ``Type'' in APL.
• Vaughan R. Pratt,Process Logic.
• Norman H. Cohen,Characterization and Elimination of Redundancy in Recursive Programs.
• Sten Andler,Predicate Path Expressions.
• Terrence C. Miller,Type Checking in an Imperfect World.
• David Harel,Recursion in Logics of Programs.
• Marco A. Casanova,Philip A. Bernstein,The Logic of a Relational Data Manipulation Language.
• Neil D. Jones,Steven S. Muchnick,Flow Analysis and Optimization of Lisp-Like Structures.
• Alfred V. Aho,Jeffrey D. Ullman,The Universality of Data Retrieval Languages.
• Rina S. Cohen,E. Harry,Automatic Generation of Near-Optimal Translators for Noncircular Attribute Grammars.
• Christoph M. Hoffmann,Michael J. O'Donnell,Interpreter Generation Using Tree Pattern Matching.
• John H. Reif,Data Flow Analysis of Communicating Processes.
• Donald I. Good,Richard M. Cohen,James Keeton-Williams,Principles of Proving Programs Correct in Gypsy.
• Amelia C. Fong,Automatic Improvement of Programs in Very High Level Languages.
• John Banning,An Efficient Way to Find Side Effects of Procedure Calls and Aliases of Variables.
• Sowmitri Swamy,John E. Savage,Space-Time Tradeoffs for Linear Recursion.
• Stanley Lee,Willem P. de Roever,Susan L. Gerhart,The Evolution of List-Copying Algorithms.
• Alfred V. Aho,Stephen N. Zilles,Barry K. Rosen,Christopher W. Fraser,A Compact, Machine-Independent Peephole Optimizer.
• Edmond Schonberg,Jacob T. Schwartz,Micha Sharir,Automatic Data Structure Selection in SETL.
• Irene Greif,Albert R. Meyer,Specifying Programming Language Semantics.
• Richard P. Reitman,Gregory R. Andrews,Certifying Information Flow Properties of Programs: An Axiomatic Approach.
• Edmund M. Clarke,Synthesis of Resource Invariants for Concurrent Programs.

1978

• Paul R. Kosinki,A Straightforward Denotational Semantics for Non-Determinant Data Flow Programs.
• Michael J. C. Gordon,Robin Milner,L. Morris,Malcolm C. Newey,Christopher P. Wadsworth,A Metalanguage for Interactive Proof in LCF.
• R. Steven Glanville,Susan L. Graham,A New Method for Compiler Code Generation.
• Daniel Ingalls,The Smalltalk-76 Programming System.
• Thomas J. Pennello,Frank DeRemer,A Forward Move Algorithm for LR Error Recovery.
• Alan J. Demers,James E. Donahue,Glenn Skinner,Data Types as Values: Polymorphism, Type-Checking, Encapsulation.
• David Harel,Vaughan R. Pratt,Nondeterminism in Logics of Programs.
• Steven M. German,Automating Proofs of the Absence of Common Runtime Errors.
• Peter J. Downey,Hanan Samet,Ravi Sethi,Off-Line and On-Line Algorithms for Deducing Equalities.
• John H. Reif,Symbolic Programming Analysis in Almost Linear Time.
• David W. Mizell,Verification and Design Aspects of ``True'' Concurrency.
• Barry K. Rosen,Monoids for Rapid Data Flow Analysis.
• Patrick Cousot,Nicolas Halbwachs,Automatic Discovery of Linear Restraints Among Variables of a Program.
• Charles G. Nelson,Derek C. Oppen,A Simplifier Based on Efficient Decision Algorithms.
• Derek C. Oppen,Reasoning about Recursively Defined Data Structures.
• Anders Haraldsson,A Partial Evaluator, Its Use for Compiling Iterative Statements in Lisp.
• Marc A. Kaplan,Jeffrey D. Ullman,A General Scheme for the Automatic Inference of Variable Types.
• Marvin H. Solomon,Type Definitions with Parameters.
• Karel Culík,Almost Control-Free (Indeterministic) Parallel Computation on Permit Schemes.
• Alfred V. Aho,Stephen N. Zilles,Thomas G. Szymanski,Leonidas J. Guibas,Douglas K. Wyatt,Compilation and Delayed Evaluation in APL.
• Stephen C. Johnson,A Portable Compiler: Theory and Practice.
• Aravind K. Joshi,Leon S. Levy,Kang Yueh,Local Constraints in the Syntax and Semantics of Programming Languages.
• Edward A. Ashcroft,William W. Wadge,Clauses: Scope Structures and Defined Functions in Lucid.
• Bhaskaram Prabhala,Ravi Sethi,Efficient Computation of Expressions with Common Subexpressions.
• John C. Reynolds,Syntactic Control of Interference.
• Robert Cartwright,Derek C. Oppen,Unrestricted Procedure Calls in Hoare's Logic.
• William F. Ogden,William E. Riddle,William C. Rounds,Complexity of Expressions Allowing Concurrency.

1977

• Jeffrey M. Barth,An Interprocedural Data Flow Analysis Algorithm.
• Patrick Cousot,Radhia Cousot,Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints.
• Thomas W. Doeppner Jr.,Parallel Program Correctness Through Refinement.
• Amelia C. Fong,Generalized Common Subexpressions in Very High Level Languages.
• Harry R. Lewis,The Equivalence Problem for Program Schemata with Nonintersecting Loops.
• Eljas Soisalon-Soininen,Elimination of Single Productions from LR Parsers in Conjunction with the Use of Default Reductions.
• John H. Reif,Harry R. Lewis,Symbolic Evaluation and the Global Value Graph.
• Anton Nijholt,On the Covering of Left Recursive Grammars.
• Robert M. Graham,Michael A. Harrison,Ravi Sethi,John C. Cherniavsky,Samuel N. Kamin,A Complete and Consistent Hoare Semantics for a Simple Programming Language.
• Barry K. Rosen,Applications of High-Level Control Flow.
• Nachum Dershowitz,Zohar Manna,The Evolution of Programs: A System for Automatic Program Modification.
• Alfred V. Aho,Stephen C. Johnson,Jeffrey D. Ullman,Code Generation for Machines with Multiregister Operations.
• Bernard Lang,Threshold Evaluation and the Semantics of Call by Value, Assignment and Generic Procedures.
• Eric C. R. Hehner,Structuring.
• Russell R. Atkinson,Carl Hewitt,Parallelism and Synchronization in Actor Systems.
• Robert Paige,Jacob T. Schwartz,Reduction in Strength of High Level Operations.
• Edmund M. Clarke,Programming Language Constructs for Which it is Impossible to Obtain "Good" Hoare-Like Axiom Systems.
• Richard A. DeMillo,Richard J. Lipton,Alan J. Perlis,Social Processes and Proofs of Theorems and Programs.
• Alan J. Demers,Generalized Left Corner Parsing.
• Gérard Berry,Jean-Jacques Lévy,Minimal and Optimal Computations of Recursive Programs.
• Norihisa Suzuki,Kiyoshi Ishihata,Implementation of an Array Bound Checker.
• Charles N. Fischer,D. R. Milton,S. B. Quiring,An Efficient Insertion-Only Error-Corrector for LL(1) Parsers.
• Ken Kennedy,Linda Zucconi,Applications of Graph Grammar for Program Control Flow Analysis.
• William H. Harrison,A New Strategy for Code Generation - The General Purpose Optimizing Compiler.
• Vaughan R. Pratt,The Competence/Performance Dichotomy in Programming.

1976

• Peter Henderson,James H. Morris Jr.,A Lazy Evaluator.
• Brenda S. Baker,An Algorithm for Structuring Programs.
• Ben Wegbreit,Goal-Directed Program Transformation.
• Amelia C. Fong,Jeffrey D. Ullman,Induction Variables in Very High Level Languages.
• Wilf R. LaLonde,On Directly Constructing LR(k) Parsers Without Chain Reductions.
• Gregory R. Ruth,Automatic Design of Data Processing Systems.
• James R. Low,Paul Rovner,Techniques for the Automatic Selection of Data Structures.
• David B. Loveman,Program Improvement by Source to Source Transformation.
• Neil D. Jones,Steven S. Muchnick,Binding Time Optimization in Programming Languages: Some Thoughts Toward the Design of an Ideal Language.
• Dianne E. Britton,Frederick C. Druseikis,Ralph E. Griswold,David R. Hanson,Richard A. Holmes,Procedure Referencing Environments in SL5.
• Robert S. Boyer,J. Strother Moore,Robert E. Shostak,Primitive Recursive Program Transformations.
• Phillip D. Summers,A Methodology for Lisp Program Construction from Examples.
• Reinhold Franck,PLAN2D - Syntactic Analysis of Precedence Graph Grammars.
• Matthew M. Geller,Test Data as an Aid in Proving Program Correctness.
• Alfred V. Aho,Stephen C. Johnson,Jeffrey D. Ullman,Code Generation for Expressions with Common Subexpressions.
• Susan L. Graham,Robert M. Graham,Michael A. Harrison,William I. Grosky,Jeffrey D. Ullman,Benton L. Leong,Detlef Wotschke,The Influence of Productions on Derivations and Parsing.
• Patricia P. Griffiths,Charles J. Prenner,Verifying Formal Specifications of Synchronous Processes.
• Ken Kennedy,Scott K. Warren,Automatic Generation of Efficient Evaluators for Attribute Grammars.
• Harry B. Hunt III,A Complexity Theory of Grammar Problems.
• Paul R. Kosinski,Mathematical Semantics and Data Flow Programming.

1975

• Glenn F. Stewart,An Algebraic Model for String Patterns.
• Richard J. Lipton,Reduction: A New Method of Proving Properties of Systems of Processes.
• Stephen A. Cook,Derek C. Oppen,An Assertion Language for Data Structures.
• Jacob T. Schwartz,Automatic Data Structure Choice in a Language of Very High Level.
• Peter E. Lauer,Roy H. Campbell,A Description of Path Expressions by Petri Nets.
• Bruce P. Lester,Program Schemas with Concurrency: Execution Time and Hangups.
• George T. Ligler,A Mathematical Approach to Language Design.
• Robert M. Graham,Michael A. Harrison,John C. Reynolds,Amelia C. Fong,John B. Kam,Jeffrey D. Ullman,Application of Lattice Algebra to Loop Optimization.
• Susan L. Gerhart,Correctness-Preserving Program Transformations.
• Ellis S. Cohen,A Semantic Model for Parallel Systems with Scheduling.
• Martin Mikelsons,Computer Assisted Application Definition.
• Patrick A. V. Hall,Peter Hitchcock,Stephen Todd,An Algebra of Relations for Machine Computation.
• Susan L. Graham,Mark N. Wegman,A Fast and Usually Linear Algorithm for Global Flow Analysis.
• D. M. Symes,New Control Structures to Aid Gotolessness.
• Ken Kennedy,Node Listings Applied to Data Flow Analysis.
• Marvin H. Solomon,Modes, Values, and Expressions.
• Harry B. Hunt III,Thomas G. Szymanski,Jeffrey D. Ullman,On the Complexity of LR(k) Testing.
• Peter Naur,Programming Languages, Natural Languages, and Mathematics.
• Neil D. Jones,Steven S. Muchnick,Even Simple Programs are Hard to Analyze.
• Mehdi Jazayeri,William F. Ogden,William C. Rounds,On the Complexity of the Circularity Test for Attribute Grammars.
• Irene Greif,Carl Hewitt,Actor Semantics of Planner-73.
• John B. Goodenough,Structured Exception Handling.

1973

• Patrick C. Fischer,Jeffrey D. Ullman,Alfred V. Aho,Stephen C. Johnson,Jeffrey D. Ullman,Deterministic Parsing of Ambiguous Grammars.
• Matthew S. Hecht,Jeffrey D. Ullman,Analysis of a Simple Algorithm for Global Flow Problems.
• Richard J. Waldinger,Karl N. Levitt,Reasoning About Programs.
• David Beech,On the Definitional Method of Standard PL/1.
• Clayton H. Lewis,Barry K. Rosen,Recursively Defined Data Types.
• Alice E. Fischer,Michael J. Fischer,Mode Modules as Representations of Domains.
• Susan L. Graham,Steven P. Rhodes,Practical Syntactic Error Recovery.
• Vaughan R. Pratt,Top Down Operator Precedence.
• John W. Backus,Programming Language Semantics and Closed Applicative Languages.
• F. Lockwood Morris,Advice on Structuring Compilers and Proving Them Correct.
• Carl Hewitt,Peter Bishop,Irene Greif,Brian Cantwell Smith,Todd Matson,Richard Steiger,Actor Induction and Meta-Evaluation.
• Andrea Maggiolo-Schettini,Barry K. Rosen,H. Raymond Strong,Procedure Linkage Optimization.
• Gloria J. Lambert,Large Scale File Processing - Pogol.
• Mario Schkolnick,Labelled Precedence Parsing.
• Gary A. Kildall,A Unified Approach to Global Program Optimization.
• Matthew M. Geller,Michael A. Harrison,Strict Deterministic Versus LR(0) Parsing.
• Louis Nolin,G. Ruggiu,Formalization of Exel.
• Robert D. Tennent,Mathematical Semantics of Snobol 4.
• Arnold L. Rosenberg,Transitions in Extendible Arrays.
• Ashok K. Chandra,On the Decision Problems of Program Schemas with Commutative and Invertable Functions.
• Mary Zosel,A Parallel Approach to Compilation.
• James H. Morris Jr.,Types are Not Sets.