Last update:
Sat Oct 14 13:13:35 MDT 2017
Robert W. Harper and
Mark Lillibridge Polymorphic Type Assignment and CPS
Conversion . . . . . . . . . . . . . . . 361--380
Bob Kessler and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 5--5
H. Abelson and
R. K. Dybvig and
C. T. Haynes and
G. J. Rozas and
N. I. Adams IV and
D. P. Friedman and
E. Kohlbecker and
G. L. Steele Jr. and
D. H. Bartley and
R. Halstead and
D. Oxley and
G. J. Sussman and
G. Brooks and
C. Hanson and
K. M. Pitman and
M. Wand Revised $^5$ Report on the Algorithmic
Language Scheme . . . . . . . . . . . . 7--105
Olivier Danvy and
Carolyn L. Talcott Introduction . . . . . . . . . . . . . . 115--116
Hayo Thielecke An Introduction to Landin's ``A
Generalization of Jumps and Labels'' . . 117--123
Peter J. Landin A Generalization of Jumps and Labels . . 125--143
Jakov Kucan Retraction Approach to CPS Transform . . 145--175
Gérard Boudol The $p$-Calculus in Direct Style . . . . 177--208
Edoardo Biagioni and
Ken Cline and
Peter Lee and
Chris Okasaki and
Chris Stone Safe-for-Space Threads in Standard ML 209--225
Luc Moreau A Syntactic Theory of Dynamic Binding 233--279
Carolyn L. Talcott Composable Semantic Models for Actor
Theories . . . . . . . . . . . . . . . . 281--343
Olivier Danvy and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 353--354
John C. Reynolds Definitional Interpreters Revisited . . 355--361
John C. Reynolds Definitional Interpreters for
Higher-Order Programming Languages . . . 363--397
Gerald Jay Sussman and
Guy L. Steele Jr. The First Report on Scheme Revisited . . 399--404
Gerald Jay Sussman and
Guy L. Steele Jr. Scheme: An Interpreter for Extended
Lambda Calculus . . . . . . . . . . . . 405--439
Olivier Danvy and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 5--5
William D. Clinger and
Anne H. Hartheimer and
Eric M. Ost Implementation Strategies for
First-Class Continuations . . . . . . . 7--45
Hayo Thielecke Using a Continuation Twice and Its
Implications for the Expressive Power of
call/cc . . . . . . . . . . . . . . . . 47--73
Mark Lillibridge Unchecked Exceptions Can Be Strictly
More Powerful Than \tt Call/CC . . . . . 75--104
Erik Sandewall An Early Use of Continuations and
Partial Evaluation for Compiling Rules
Written in First-Order Predicate
Calculus . . . . . . . . . . . . . . . . 105--113
Olivier Danvy and
Carolyn Talcott Introduction . . . . . . . . . . . . . . 123--124
Gilles Barthe and
John Hatcliff and
Morten Heine B. Sòrensen CPS Translations and Applications: The
Cube and Beyond . . . . . . . . . . . . 125--170
Ian A. Mason Computing with Contexts . . . . . . . . 171--201
C. S. Lee Partial Evaluation of the Euclidean
Algorithm, Revisited . . . . . . . . . . 203--212
Olivier Danvy and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 219--219
Guy L. Steele Jr. Growing a Language . . . . . . . . . . . 221--236
Alexander Aiken and
Edward L. Wimmers and
Jens Palsberg Optimal Representations of Polymorphic
Types with Subtyping . . . . . . . . . . 237--282
Mitchell Wand Continuation-Based Multiprocessing
Revisited . . . . . . . . . . . . . . . 283--283
Mitchell Wand Continuation-Based Multiprocessing . . . 285--299
Olivier Danvy and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 307--308
Sandrine Chirokoff and
Charles Consel and
Renaud Marlet Combining Program and Data
Specialization . . . . . . . . . . . . . 309--335
Luke Hornof and
Trevor Jim Certifying Compilation and Run-Time Code
Generation . . . . . . . . . . . . . . . 337--375
Yoshihiko Futamura Partial Evaluation of Computation
Process, Revisited . . . . . . . . . . . 377--380
Yoshihiko Futamura Partial Evaluation of Computation
Process --- An Approach to a
Compiler-Compiler . . . . . . . . . . . 381--391
Olivier Danvy and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 5--6
Peter D. Mosses A Foreword to ``Fundamental Concepts in
Programming Languages'' . . . . . . . . 7--9
Christopher Strachey Fundamental Concepts in Programming
Languages . . . . . . . . . . . . . . . 11--49
Rod Burstall Christopher Strachey --- Understanding
Programming Languages . . . . . . . . . 51--55
R. Kent Dybvig From Macrogeneration to Syntactic
Abstraction . . . . . . . . . . . . . . 57--63
Mike Gordon Christopher Strachey: Recollections of
His Influence . . . . . . . . . . . . . 65--67
David Hartley Cambridge and CPL in the 1960s . . . . . 69--70
C. A. R. Hoare A Hard Act to Follow . . . . . . . . . . 71--72
Michael Jackson Christopher Strachey: a Personal
Recollection . . . . . . . . . . . . . . 73--74
Peter J. Landin My Years with Strachey . . . . . . . . . 75--76
Robert Milne From Language Concepts to Implementation
Concepts . . . . . . . . . . . . . . . . 77--81
Roger Penrose Reminiscences of Christopher Strachey 83--84
Martin Richards Christopher Strachey and the Cambridge
CPL Compiler . . . . . . . . . . . . . . 85--88
David A. Schmidt Induction, Domains, Calculi: Strachey's
Contributions to Programming-Language
Engineering . . . . . . . . . . . . . . 89--101
Dana Scott Some Reflections on Strachey and His
Work . . . . . . . . . . . . . . . . . . 103--114
Joe Stoy Christopher Strachey and Fundamental
Concepts . . . . . . . . . . . . . . . . 115--117
Robert D. Tennent and
Dan R. Ghica Abstract Models of Storage . . . . . . . 119--129
Christopher P. Wadsworth Continuations Revisited . . . . . . . . 131--133
Christopher Strachey and
Christopher P. Wadsworth Continuations: a Mathematical Semantics
for Handling Full Jumps . . . . . . . . 135--152
Olivier Danvy and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 159--160
Scott Thibault and
Charles Consel and
Julia L. Lawall and
Renaud Marlet and
Gilles Muller Static and Dynamic Program Compilation
by Interpreter Specialization . . . . . 161--178
John Hannan and
Patrick Hicks Higher-Order UnCurrying . . . . . . . . 179--216
Torben Æ. Mogensen Linear-Time Self-Interpretation of the
Pure Lambda Calculus . . . . . . . . . . 217--237
Shin-Ya Nishizaki A Polymorphic Environment Calculus and
its Type-Inference Algorithm . . . . . . 239--278
Olivier Danvy and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 287--288
Yanhong A. Liu Efficiency by Incrementalization: An
Introduction . . . . . . . . . . . . . . 289--313
John Hatcliff and
Matthew B. Dwyer and
Hongjun Zheng Slicing Software for Model Construction 315--353
Torben Æ. Mogensen Glossary for Partial Evaluation and
Related Topics . . . . . . . . . . . . . 355--368
Olivier Danvy and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 5--5
Rémi Douence and
Mario Südholt A Generic Reification Technique for
Object-Oriented Reflective Languages . . 7--34
Jerzy Karczmarczuk Functional Differentiation of Computer
Programs . . . . . . . . . . . . . . . . 35--57
Andrei Sabelfeld and
David Sands A Per Model of Secure Information Flow
in Sequential Programs . . . . . . . . . 59--91
Olivier Danvy and
Julia L. Lawall Editorial . . . . . . . . . . . . . . . 99--100
Eijiro Sumii and
Naoki Kobayashi A Hybrid Approach to Online and Offline
Partial Evaluation . . . . . . . . . . . 101--142
John P. Gallagher and
Julio C. Peralta Regular Tree Languages as an Abstract
Domain in Program Specialisation . . . . 143--172
Bernd Grobauer and
Zhe Yang The Second Futamura Projection for
Type-Directed Partial Evaluation . . . . 173--219
Naoki Kobayashi Type-Based Useless-Variable Elimination 221--260
Wei-Ngan Chin and
Siau-Cheng Khoo Calculating Sized Types . . . . . . . . 261--300
Olivier Danvy and
Takayasu Ito and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 307--307
Edoardo Biagioni and
Robert Harper and
Peter Lee A Network Protocol Stack in Standard ML 309--356
Luc Moreau Tree Rerooting in Distributed Garbage
Collection: Implementation and
Performance Evaluation . . . . . . . . . 357--386
Yong Xiao and
Amr Sabry and
Zena M. Ariola From Syntactic Theories to Interpreters:
Automating the Proof of Unique
Decomposition . . . . . . . . . . . . . 387--409
Olivier Danvy and
Takayasu Ito and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 5--5
Akihiko Tozawa and
Masami Hagiya Formalization and Analysis of Class
Loading in Java . . . . . . . . . . . . 7--55
Catarina Coquand A Formalised Proof of the Soundness and
Completeness of a Simply Typed
Lambda-Calculus with Explicit
Substitutions . . . . . . . . . . . . . 57--90
Hongwei Xi Dependent Types for Program Termination
Verification . . . . . . . . . . . . . . 91--131
Olivier Danvy and
Amr Sabry Editorial . . . . . . . . . . . . . . . 139--140
Hayo Thielecke Comparing Control Constructs by
Double-Barrelled CPS . . . . . . . . . . 141--160
John Reppy Optimizing Nested Loops Using Local CPS
Conversion . . . . . . . . . . . . . . . 161--180
Josh Berdine and
Peter O'Hearn and
Uday Reddy and
Hayo Thielecke Linear Continuation-Passing . . . . . . 181--208
Steve Zdancewic and
Andrew C. Myers Secure Information Flow via Linear
Continuations . . . . . . . . . . . . . 209--234
Masahito Hasegawa and
Yoshihiko Kakutani Axioms for Recursion in Call-by-Value 235--264
Olivier Danvy and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 271--271
Patricia Johann A Generalization of Short-Cut Fusion and
its Correctness Proof . . . . . . . . . 273--300
Scott F. Smith and
Carolyn L. Talcott Specification Diagrams for Actor Systems 301--348
Peter Henderson Functional Geometry . . . . . . . . . . 349--365
Olivier Danvy and
Fritz Henglein and
Harry Mairson and
Alberto Pettorossi Editorial . . . . . . . . . . . . . . . 5--6
Bob Paige Research Retrospective . . . . . . . . . 7--13
Oege de Moor and
David Lacey and
Eric Van Wyk Universal Regular Path Queries . . . . . 15--35
Yanhong A. Liu and
Scott D. Stoller Dynamic Programming via Static
Incrementalization . . . . . . . . . . . 37--62
Elizabeth I. Leonard and
Constance L. Heitmeyer Program Synthesis from Formal
Requirements Specifications Using APTS 63--92
Thomas W. Reps and
Louis B. Rall Computational Divided Differencing and
Divided-Difference Arithmetics . . . . . 93--149
David Basin and
Olivier Danvy and
Julian Padget and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 159--159
Jonathan Ford and
Ian A. Mason Formal Foundations of Operational
Semantics . . . . . . . . . . . . . . . 161--202
H.-W. Loidl and
F. Rubio and
N. Scaife and
K. Hammond and
S. Horiguchi and
U. Klusik and
R. Loogen and
G. J. Michaelson and
R. Peña and
S. Priebe and
Á. J. Rebón and
P. W. Trinder Comparing Parallel Functional Languages:
Programming and Performance . . . . . . 203--251
Inge Li Gòrtz and
Signe Reuss and
Morten Heine Sòrensen Strong Normalization from Weak
Normalization by Translation into the
Lambda-I-Calculus . . . . . . . . . . . 253--285
Olivier Danvy and
Peter Thiemann Editorial . . . . . . . . . . . . . . . 295--295
Roberto Giacobazzi and
Isabella Mastroeni Non-Standard Semantics for Program
Slicing . . . . . . . . . . . . . . . . 297--339
Lunjin Lu Path Dependent Analysis of Logic
Programs . . . . . . . . . . . . . . . . 341--377
Aleksandar Nanevski and
Guy Blelloch and
Robert Harper Automatic Generation of Staged Geometric
Predicates . . . . . . . . . . . . . . . 379--400
Robert Harper and
Mark Lillibridge Corrigendum: Polymorphic Type Assignment
and CPS Conversion . . . . . . . . . . . 401--401
Wei-Ngan Chin and
Olivier Danvy and
Peter Thiemann Editorial . . . . . . . . . . . . . . . 5--6
Germán Vidal Cost--Augmented Partial Evaluation of
Functional Logic Programs . . . . . . . 7--46
Anne-Françoise Le Meur and
Julia L. Lawall and
Charles Consel Specialization Scenarios: a Pragmatic
Approach to Declaring Program
Specialization . . . . . . . . . . . . . 47--92
Siau-Cheng Khoo and
Kun Shi Program Adaptation via Output-Constraint
Specialization . . . . . . . . . . . . . 93--128
Janis Voigtländer Using Circular Programs to Deforest in
Accumulating Parameters . . . . . . . . 129--163
David Basin and
Olivier Danvy and
Robert Harper Editorial . . . . . . . . . . . . . . . 171--171
David Lacey and
Neil D. Jones and
Eric Van Wyk and
Carl Christian Frederiksen Compiler Optimization Correctness by
Temporal Logic . . . . . . . . . . . . . 173--206
Lars Michael Kristensen and
Sòren Christensen Implementing Coloured Petri Nets Using a
Functional Programming Language . . . . 207--243
Mads Tofte and
Lars Birkedal and
Martin Elsman and
Niels Hallenberg A Retrospective on Region-Based Memory
Management . . . . . . . . . . . . . . . 245--265
Olivier Danvy and
Ian Mason Editorial . . . . . . . . . . . . . . . 275--275
Christian Queinnec Continuations and Web Servers . . . . . 277--295
Isabella Mastroeni Algebraic Power Analysis by Abstract
Interpretation . . . . . . . . . . . . . 297--345
Simon Helsen Bisimilarity for the Region Calculus . . 347--394
Olivier Danvy and
Fritz Henglein and
Harry Mairson and
Alberto Pettorossi Editorial . . . . . . . . . . . . . . . 5--6
Harry Mairson Robert Paige (1947--1999) . . . . . . . 7--8
Alan Siegel Remembrances of Bob Paige . . . . . . . 9--11
Martin Davis An Appreciation of Bob Paige . . . . . . 13--13
Deepak Goyal Transformational Derivation of an
Improved Alias Analysis Algorithm . . . 15--49
Jules Desharnais and
Bernhard Möller Least Reflexive Points of Relations . . 51--77
Nils Klarlund Relativizations for the Logic-Automata
Connection . . . . . . . . . . . . . . . 79--120
Alberto Pettorossi and
Maurizio Proietti and
Sophie Renault Derivation of Efficient Logic Programs
by Specialization and Reduction of
Nondeterminism . . . . . . . . . . . . . 121--210
Robert Paige An NSF Proposal . . . . . . . . . . . . 211--235
Matthias Felleisen and
Julia Lawall and
Manuel Serrano and
Olin Shivers Editorial . . . . . . . . . . . . . . . 243--244
Philippe Meunier and
Robert Bruce Findler and
Paul Steckler and
Mitchell Wand Selectors Make Set--Based Analysis Too
Hard . . . . . . . . . . . . . . . . . . 245--269
Danny Dubé and
Marc Feeley BIT: a Very Compact Scheme System for
Microcontrollers . . . . . . . . . . . . 271--298
Oscar Waddell and
Dipanwita Sarkar and
R. Kent Dybvig Fixing Letrec: a Faithful Yet Efficient
Implementation of Scheme's Recursive
Binding Construct . . . . . . . . . . . 299--326
Martin Gasbichler and
Michael Sperber Integrating User-Level Threads with
Processes in Scsh . . . . . . . . . . . 327--354
Oleg Kiselyov Implementing Metcast in Scheme . . . . . 355--370
Mayer Goldberg A Variadic Extension of Curry's
Fixed-Point Combinator . . . . . . . . . 371--388
Olivier Danvy and
Oege de Moor and
Julian Padget and
Peter Thiemann Editorial . . . . . . . . . . . . . . . 5--5
Matthieu Martel Semantics of roundoff error propagation
in finite precision calculations . . . . 7--30
Antoine Miné The octagon abstract domain . . . . . . 31--100
V. Krishna Nandivada and
Suresh Jagannathan Dynamic state restoration using
versioning exceptions . . . . . . . . . 101--124
François Pottier and
Nadji Gauthier Polymorphic typed defunctionalization
and concretization . . . . . . . . . . . 125--162
Furio Honsell and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 167--168
Michael Norrish Mechanising $\lambda$-calculus using a
classical first order theory of terms
with permutations . . . . . . . . . . . 169--195
Jason Hickey and
Aleksey Nogin Formal compiler construction in a
logical framework . . . . . . . . . . . 197--230
Makoto Hamana An initial algebra approach to term
rewriting systems with variable binders 231--262
Neil Ghani and
Tarmo Uustalu and
Makoto Hamana Explicit substitutions and higher-order
syntax . . . . . . . . . . . . . . . . . 263--282
Fabio Gadducci and
Marino Miculan and
Ugo Montanari About permutation algebras, (pre)sheaves
and named sets . . . . . . . . . . . . . 283--304
Miki Tanaka and
John Power Pseudo-distributive laws and axiomatics
for variable binding . . . . . . . . . . 305--337
Olivier Danvy and
Andrzej Filinski and
Jean-Louis Giavitto and
Andy King and
Pierre-Etienne Moreau and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 343--344
Clara Bertolissi and
Horatiu Cirstea and
Claude Kirchner Expressing combinatory reduction systems
derivations in the rewriting calculus 345--376
Paul Blain Levy Call-by-push-value: Decomposing
call-by-value and call-by-name . . . . . 377--414
Patricia M. Hill and
Fausto Spoto Deriving escape analysis by abstract
interpretation . . . . . . . . . . . . . 415--463
Narciso Martí-Oliet and
Grigore Rosu and
Carolyn Talcott Editorial . . . . . . . . . . . . . . . 1--2
Iliano Cervesato and
Mark-Oliver Stehr Representing the MSR cryptoprotocol
specification language in an extension
of rewriting logic with dependent types 3--35
Horatiu Cirstea and
Germain Faure and
Claude Kirchner A $\rho$-calculus of explicit constraint
application . . . . . . . . . . . . . . 37--72
Francisco J. López Fraguas and
Mario Rodríguez Artalejo and
Rafael del Vado Vírseda A new generic scheme for functional
logic programming with constraints . . . 73--122
José Meseguer and
Prasanna Thati Symbolic reachability analysis using
narrowing and its application to
verification of cryptographic protocols 123--160
Peter Csaba Ölveczky and
José Meseguer Semantics and pragmatics of Real-Time
Maude . . . . . . . . . . . . . . . . . 161--196
Olivier Danvy Editorial . . . . . . . . . . . . . . . 197--198
Jean-Louis Krivine A call-by-name lambda-calculus machine 199--207
Pierre Crégut Strongly reducing variants of the
Krivine abstract machine . . . . . . . . 209--230
Mitchell Wand On the correctness of the Krivine
machine . . . . . . . . . . . . . . . . 231--235
Rémi Douence and
Pascal Fradet The next 700 Krivine machines . . . . . 237--255
Frédéric Lang Explaining the lazy Krivine machine
using explicit substitution and
addresses . . . . . . . . . . . . . . . 257--270
Daniel P. Friedman and
Abdulaziz Ghuloum and
Jeremy G. Siek and
Onnie Lynn Winebarger Improving the lazy Krivine machine . . . 271--293
Sylvain Lippi The graphical Krivine machine . . . . . 295--318
David A. Schmidt State-transition machines for
lambda-calculus expressions . . . . . . 319--332
David A. Schmidt State-transition machines, revisited . . 333--335
Olivier Danvy and
Hayo Thielecke Editorial . . . . . . . . . . . . . . . 337--338
Yukiyoshi Kameyama Axioms for control operators in the CPS
hierarchy . . . . . . . . . . . . . . . 339--369
Chung-chieh Shan A static simulation of dynamic delimited
control . . . . . . . . . . . . . . . . 371--401
Zena M. Ariola and
Hugo Herbelin and
Amr Sabry A proof-theoretic foundation of abortive
continuations . . . . . . . . . . . . . 403--429
Shriram Krishnamurthi and
Peter Walton Hopkins and
Jay McCarthy and
Paul T. Graunke and
Greg Pettyjohn and
Matthias Felleisen Implementation and use of the PLT scheme
Web server . . . . . . . . . . . . . . . 431--460
Julia Lawall and
Michael Leuschel and
Peter Sestoft Editorial . . . . . . . . . . . . . . . 1--3
Steve Barker and
Michael Leuschel and
Mauricio Varea Efficient and flexible access control
via Jones-optimal logic program
specialisation . . . . . . . . . . . . . 5--35
Sòren Debois Imperative-program transformation by
instrumented-interpreter specialization 37--58
Francisco Durán and
Salvador Lucas and
Claude Marché and
José Meseguer and
Xavier Urbain Proving operational termination of
membership equational programs . . . . . 59--88
Zhenjiang Hu and
Shin-Cheng Mu and
Masato Takeichi A programmable editor for developing
structured documents based on
bidirectional transformations . . . . . 89--118
Jarle Hulaas and
Walter Binder Program transformations for light-weight
CPU accounting and control in the Java
Virtual Machine . . . . . . . . . . . . 119--146
Claudio Ochoa and
Josep Silva and
Germán Vidal Dynamic slicing of lazy functional
programs based on redex trails . . . . . 147--192
Alberto Pettorossi and
Maurizio Proietti Totally correct logic program
transformations via well-founded
annotations . . . . . . . . . . . . . . 193--234
Alberto Pettorossi and
Maurizio Proietti Totally correct logic program
transformations via well-founded
annotations . . . . . . . . . . . . . . 235--235
Olivier Danvy and
R. Kent Dybvig and
Julia Lawall and
Peter Thiemann Editorial . . . . . . . . . . . . . . . 237--238
Christian Skalka Types and trace effects for object
orientation . . . . . . . . . . . . . . 239--282
Robert Glück An investigation of Jones optimality and
BTI-universal specializers . . . . . . . 283--309
Christian H. Bischof and
Paul D. Hovland and
Boyana Norris On the implementation of automatic
differentiation tools . . . . . . . . . 311--331
Lukasz Ziarek and
Stephen Weeks and
Suresh Jagannathan Flattening tuples in an SSA intermediate
representation . . . . . . . . . . . . . 333--358
Olivier Danvy and
Ian Mason Editorial . . . . . . . . . . . . . . . 359--359
Jeffrey Mark Siskind and
Barak A. Pearlmutter Nesting forward-mode AD in a functional
framework . . . . . . . . . . . . . . . 361--376
Scott Owens and
Konrad Slind Adapting functional programs to higher
order logic . . . . . . . . . . . . . . 377--409
Torben Amtoft Flow-sensitive type systems and the
ambient calculus . . . . . . . . . . . . 411--442
Olivier Danvy and
Julian Padget Editorial . . . . . . . . . . . . . . . 1--1
Tom Hirschowitz and
Xavier Leroy and
J. B. Wells Compilation of extended recursion in
call-by-value functional languages . . . 3--66
Matthew Naylor and
Colin Runciman Expressible sharing for functional
circuit description . . . . . . . . . . 67--80
Jean Bresson and
Carlos Agon and
Gérard Assayag Visual Lisp/CLOS programming in
OpenMusic . . . . . . . . . . . . . . . 81--111
Olivier Danvy and
Carolyn L. Talcott Editorial . . . . . . . . . . . . . . . 113--113
Aaron Stump Directly reflective meta-programming . . 115--144
David Monniaux A minimalistic look at widening
operators . . . . . . . . . . . . . . . 145--154
Patricia Johann and
Neil Ghani A principled approach to programming
with nested types in Haskell . . . . . . 155--189
Olivier Danvy Peter J. Landin (1930--2009) . . . . . . 191--195
Olivier Danvy and
Carolyn L. Talcott Editorial . . . . . . . . . . . . . . . 197--197
Zaynah Dargaye and
Xavier Leroy A verified framework for higher-order
uncurrying optimizations . . . . . . . . 199--231
Zena M. Ariola and
Hugo Herbelin and
Amr Sabry A type-theoretic foundation of delimited
continuations . . . . . . . . . . . . . 233--273
Kenichi Asai On typing delimited continuations: three
new solutions to the printf problem . . 275--291
Olivier Danvy and
Carolyn L. Talcott Editorial . . . . . . . . . . . . . . . 293--293
Richard Bornat Peter Landin: a computer scientist who
inspired a generation . . . . . . . . . 295--298
Paul P. Boca Personal recollections of Peter Landin:
1987--2009 . . . . . . . . . . . . . . . 299--303
Kevin Hammond and
Greg Michaelson The Peter Landin Prize . . . . . . . . . 305--312
R. D. Tennent An introduction to Landin's ``Getting
Rid of Labels'' . . . . . . . . . . . . 313--314
P. J. Landin Getting rid of labels . . . . . . . . . 315--329
Tony Clark Stories about calculations: remembering
Peter Landin . . . . . . . . . . . . . . 331--332
Peter J. Landin Calculations: a Hole in the Heart of the
Study of Computing . . . . . . . . . . . 333--359
Sandra Alves and
Maribel Fernández and
Mário Florido and
Ian Mackie Linearity and iterator types for Gödel's
System . . . . . . . . . . . . . . . . . 1--27
Fausto Spoto and
Étienne Payet Magic-sets for localised analysis of
Java bytecode . . . . . . . . . . . . . 29--86
Axel Simon and
Andy King The two variable per inequality abstract
domain . . . . . . . . . . . . . . . . . 87--143
Arie Middelkoop and
Atze Dijkstra and
S. Doaitse Swierstra A lean specification for GADTs: system F
with first-class equality proofs . . . . 145--166
David Herman and
Aaron Tomb and
Cormac Flanagan Space-efficient gradual typing . . . . . 167--189
Gudmund Grov and
Greg Michaelson Hume box calculus: robust system
development through software
transformation . . . . . . . . . . . . . 191--226
Neil Sculthorpe and
Henrik Nilsson Keeping calm in the face of change:
Towards optimisation of FRP by reasoning
about change . . . . . . . . . . . . . . 227--271
John P. Gallagher and
Janis Voigtländer Editorial . . . . . . . . . . . . . . . 273--274
Arun Lakhotia and
Davidson R. Boccardo and
Anshuman Singh and
Aleardo Manacero Context-sensitive analysis without
calling-context . . . . . . . . . . . . 275--313
Stefan Holdermans and
Jurriaan Hage Making ``stricterness'' more relevant 315--335
Fritz Henglein and
Ken Friis Larsen Generic multiset programming with
discrimination-based joins and symbolic
Cartesian products . . . . . . . . . . . 337--370
Johannes Rudolph and
Peter Thiemann Mnemonics: type-safe bytecode generation
at run time . . . . . . . . . . . . . . 371--407
Manuel Serrano and
Christian Queinnec A multi-tier semantics for Hop . . . . . 409--431
Bryan Chadwick and
Karl Lieberherr A functional approach to generic
programming using adaptive traversals 433--463
Peter Achten and
Marko van Eekelen and
Pieter Koopman and
Marco T. Morazán Trends in Trends in Functional
Programming 1999/2000 versus 2007/2008 465--487
Wouter Swierstra More dependent types for distributed
arrays . . . . . . . . . . . . . . . . . 489--506
Julia Lawall and
Germán Puebla and
Germán Vidal Editorial . . . . . . . . . . . . . . . 1--2
Nabil el Boustani and
Jurriaan Hage Improving type error messages for
generic Java . . . . . . . . . . . . . . 3--39
Robert J. Simmons and
Frank Pfenning Logical approximation for program
analysis . . . . . . . . . . . . . . . . 41--80
Cherif Salama and
Gregory Malecha and
Walid Taha and
Jim Grundy and
John O'Leary Static consistency checking for Verilog
wire interconnects: Using dependent
types to check the sanity of Verilog
descriptions . . . . . . . . . . . . . . 81--114
Alberto Pardo and
João Paulo Fernandes and
João Saraiva Shortcut fusion rules for the derivation
of circular and higher-order programs 115--149
Kung Chen and
Shu-Chun Weng and
Jia-Yin Lin and
Meng Wang and
Siau-Cheng Khoo Side-effect localization for lazy,
purely functional languages via aspects 151--189
M. Niqui and
J. J. M. M. Rutten A proof of Moessner's theorem by
coinduction . . . . . . . . . . . . . . 191--206
Jacques Garrigue and
Keiko Nakata Path resolution for nested recursive
modules . . . . . . . . . . . . . . . . 207--237
Gabriel Kerneis and
Juliusz Chroboczek Continuation-Passing C, compiling
threads to events through continuations 239--279
Hideya Iwasaki and
Takeshi Morimoto and
Yasunao Takano Pruning with improving sequences in lazy
functional programs . . . . . . . . . . 281--309
Kenichi Asai and
Oleg Kiselyov and
Chung-chieh Shan Functional un$|$unparsing . . . . . . . 311--340
Yu David Liu and
Christian Skalka and
Scott F. Smith Type-specialized staged programming with
process separation . . . . . . . . . . . 341--385
Gabriel Kerneis and
Juliusz Chroboczek Erratum to: Continuation--Passing C,
compiling threads to events through
continuations . . . . . . . . . . . . . 387--387
Oleg Kiselyov and
Julia Lawall and
Simon Thompson Editorial PEPM2012 . . . . . . . . . . . 1--2
Kazutaka Matsuda and
Kazuhiro Inaba and
Keisuke Nakano Polynomial-time inverse computation for
accumulative functions with multiple
data traversals . . . . . . . . . . . . 3--38
Naoki Kobayashi and
Kazutaka Matsuda and
Ayumi Shinohara Functional programs as compressed data 39--84
Markus Degen and
Peter Thiemann and
Stefan Wehr The interaction of contracts and
laziness . . . . . . . . . . . . . . . . 85--125
Isao Sasano and
Takumi Goto An approach to completing variable names
for implicitly typed functional
languages . . . . . . . . . . . . . . . 127--163
Tiark Rompf and
Nada Amin and
Adriaan Moors Scala-Virtualized: linguistic reuse for
deep embeddings . . . . . . . . . . . . 165--207
Casey Klein and
Matthew Flatt and
Robert Bruce Findler The Racket virtual machine and
randomized testing . . . . . . . . . . . 209--253
Andy Gill and
Tristan Bull and
Andrew Farmer Types and associated type families for
hardware simulation and synthesis . . . 255--274
John Capper and
Henrik Nilsson Structural types for systems of
equations . . . . . . . . . . . . . . . 275--310
Viktória Zsók and
Rex Page and
Julia Lawall Editorial TFP 2009/2010 . . . . . . . . 1--2
Thomas Horstmeyer and
Rita Loogen Graph-based communication in Eden . . . 3--28
Silvia Clerici and
Cristina Zoltan Graphical and incremental type
inference. A graph transformation
approach . . . . . . . . . . . . . . . . 29--62
Ian Zerny On graph rewriting, reduction, and
evaluation in the presence of cycles . . 63--84