Last update:
Mon May 27 11:27:17 MDT 2024
Anonymous Editorial . . . . . . . . . . . . . . . 1--2
F. Warren Burton Encapsulating non-determinacy in an
abstract data type with determinate
semantics . . . . . . . . . . . . . . . 3--20
Carsten K. Gomard and
Neil D. Jones A partial evaluator for the untyped
lambda-calculus . . . . . . . . . . . . 21--69
Mikael Rittri Using types as search keys in function
libraries . . . . . . . . . . . . . . . 71--89
Sebastian Hunt and
Chris Hankin Fixed points and frontiers: a new
perspective . . . . . . . . . . . . . . 91--120
Richard S. Bird Functional Pearls: The Minout problem 121--124
Anonymous JFP volume 1 issue 1 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 1 issue 1 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b6
Henk Barendregt Introduction to generalized type systems 125--154
Herman Geuvers and
Mark-Jan Nederhof Modular proof of strong normalization
for the calculus of constructions . . . 155--189
Colin Runciman and
Ian Toyn Retrieving reusable software components
by polymorphic type . . . . . . . . . . 191--211
François Major and
Guy Lapalme and
Robert Cedergren Domain generating functions for solving
constraint satisfaction problems . . . . 213--227
Henk Barendregt Theoretical Pearls: Self-interpretation
in lambda calculus . . . . . . . . . . . 229--233
Richard S. Bird Functional Pearls: On removing
duplicates . . . . . . . . . . . . . . . 235--243
Anonymous JFP volume 1 issue 2 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 1 issue 2 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
John C. Mitchell Type inference with simple subtypes . . 245--285
Ian Mason and
Carolyn Talcott Equivalence in functional languages with
effects . . . . . . . . . . . . . . . . 287--327
G. L. Burn Implementing the evaluation transformer
model of reduction on parallel machines 329--366
Erik Barendsen Theoretical Pearls: An unsolvable
numeral system in lambda calculus . . . 367--372
Anonymous Errataum . . . . . . . . . . . . . . . . 373--373
Anonymous JFP volume 1 issue 3 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 1 issue 3 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b4
M. Abadi and
L. Cardelli and
P.-L. Curien and
J.-J. Lévy Explicit substitutions . . . . . . . . . 375--416
Luca Cardelli and
Giuseppe Longo A semantic basis for Quest . . . . . . . 417--458
Hanne Riis Nielson and
Flemming Nielson Using transformations in the
implementation of higher-order functions 459--494
Anonymous Author Index to Volume 1 . . . . . . . . 495--495
Anonymous JFP volume 1 issue 4 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 1 issue 4 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b7
Manfred Broy and
Claus Dendorfer Modelling operating system structures by
timed stream processing functions . . . 1--21
Andrea Asperti A categorical understanding of
environment machines . . . . . . . . . . 23--59
Roger L. Wainwright and
Marian E. Sexton A study of sparse matrix representations
for solving linear systems in a
functional language . . . . . . . . . . 61--72
Richard Jones Tail recursion without space leaks . . . 73--79
James M. Boyle and
Terence J. Harmer A practical functional program for the
CRAY X-MP . . . . . . . . . . . . . . . 81--126
Andrew W. Appel and
Robert Harper Special Issue on ML . . . . . . . . . . i
Anonymous JFP volume 2 issue 1 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 2 issue 1 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b3
Simon L. Peyton Jones Implementing lazy functional languages
on stock hardware: the Spineless Tagless
G-machine . . . . . . . . . . . . . . . 127--202
F. Warren Burton and
Rex L. Page Distributed random number generation . . 203--212
Harry G. Mairson Quantifier elimination and parametric
polymorphism in programming languages 213--226
Thomas Johnson A review of the FPCA '91 proceedings ---
Hughes John (Ed); \booktitleFunctional
Programming Languages and Computer
Architecture. Proceedings of the fifth
conference (Cambridge, MA, 28-30081991),
Volume 523 of Lecture Notes in Computer
Science, Springer-Verlag. 666 pp. . . . 227--231
Henk Barendregt Theoretical Pearls: Enumerators of
lambda terms are reducing . . . . . . . 233--236
R. S. Bird Functional Pearls: Two greedy algorithms 237--244
Anonymous JFP volume 2 issue 2 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 2 issue 2 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b4
Jean-Pierre Talpin and
Pierre Jouvelot Polymorphic type, region and effect
inference . . . . . . . . . . . . . . . 245--271
Frank S. K. Silbermann and
Bharat Jayaraman A domain-theoretic approach to
functional and logic programming . . . . 273--321
Graham Hutton Higher-order functions for parsing . . . 323--343
Torben Æ. Mogensen Efficient self-interpretation in lambda
calculus . . . . . . . . . . . . . . . . 345--364
Neil D. Jones Book Review: \booktitleProjection
Factorisations in Partial Evaluation. By
John Launchbury. Distinguished
Dissertations in Computer Science, Vol.
1. Cambridge University Press, 1991.
ISBN 0-521-41497-0 . . . . . . . . . . . 365--365
Henk Barendregt Theoretical Pearls: Representing
`undefined' in lambda calculus . . . . . 367--374
Richard S. Bird Functional Pearls: Unravelling greedy
algorithms . . . . . . . . . . . . . . . 375--385
Anonymous JFP volume 2 issue 3 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 2 issue 3 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b4
Gad Aharoni and
Dror G. Feitelson and
Amnon Barak A run-time algorithm for managing the
granularity of parallel functional
programs . . . . . . . . . . . . . . . . 387--405
François Bourdoncle Abstract interpretation by dynamic
partitioning . . . . . . . . . . . . . . 407--435
P. J. Brumfitt Metamorph --- a formal methods toolkit
with application to the design of
digital hardware . . . . . . . . . . . . 437--473
Mark P. Jones Computing with lattices: An application
of type classes . . . . . . . . . . . . 475--503
Rob R. Hoogerwoord Functional Pearls: A symmetric set of
efficient list operations . . . . . . . 505--513
Anonymous Author Index to Volume 2 . . . . . . . . 515--515
Anonymous JFP volume 2 issue 4 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 2 issue 4 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b3
Henk Barendregt and
Paul Hudak and
John Hughes and
Simon Peyton Jones and
Philip Wadler Editorial . . . . . . . . . . . . . . . 1--2
Simon Thompson and
Philip Wadler Functional programming in education ---
Introduction . . . . . . . . . . . . . . 3--4
Tim Lambert and
Peter Lindsay and
Ken Robinson Using Miranda as a first programming
language . . . . . . . . . . . . . . . . 5--34
Phil Molyneux Functional programming for business
students . . . . . . . . . . . . . . . . 35--48
Stef Joosten and
Klaas Van Den Berg and
Gerrit Van Der Hoeven Teaching functional programming to
first-year students . . . . . . . . . . 49--65
Rachel Harrison The use of functional languages in
teaching computer science . . . . . . . 67--75
Lennart Augustsson The interactive Lazy ML system . . . . . 77--92
Colin Runciman and
Ian Toyn and
Mike Firth An incremental, exploratory and
transformational environment for lazy
functional programming . . . . . . . . . 93--115
R. S. Bird Functional Pearls: The last tail . . . . 117--122
Anonymous JFP volume 3 issue 1 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 3 issue 1 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b4
John Hannan Extended natural semantics . . . . . . . 123--152
W. Ken Jackson and
F. Warren Burton Improving intervals . . . . . . . . . . 153--169
F. Warren Burton and
Robert D. Cameron Pattern matching with abstract data
types . . . . . . . . . . . . . . . . . 171--190
Eric Nöcker and
Sjaak Smetsers Partially strict non-recursive data
types . . . . . . . . . . . . . . . . . 191--215
Colin Runciman and
David Wakeling Heap profiling of lazy functional
programs . . . . . . . . . . . . . . . . 217--245
Chris Reade Terminating comprehensions . . . . . . . 247--250
Anonymous JFP volume 3 issue 2 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 3 issue 2 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
Erik Ruf and
Daniel Weise On the specialization of online program
specializers . . . . . . . . . . . . . . 251--281
Valentin F. Turchin Program transformation with metasystem
transitions . . . . . . . . . . . . . . 283--313
Anders Bondorf and
Jesper Jòrgensen Efficient analyses for realistic
off-line partial evaluation . . . . . . 315--346
Jens Palsberg Correctness of binding-time analysis . . 347--363
Mitchell Wand Specifying the correctness of
binding-time analysis . . . . . . . . . 365--387
Anonymous JFP volume 3 issue 3 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 3 issue 3 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
Andrew W. Appel and
Robert Harper Special Issue on ML . . . . . . . . . . 389--389
Neil Jones Erratum . . . . . . . . . . . . . . . . 389--389
Andrew W. Appel A critique of Standard ML . . . . . . . 391--429
Xavier Leroy and
Michel Mauny Dynamics in ML . . . . . . . . . . . . . 431--463
Robert Harper and
Bruce F. Duba and
David Macqueen Typing first-class continuations in ML 465--484
Roberto Di Cosmo Deciding type isomorphisms in a
type-assignment framework . . . . . . . 485--525
Dave Berry Lessons from the design of a Standard ML
library . . . . . . . . . . . . . . . . 527--552
Stephen Adams Functional Pearls: Efficient sets --- a
balancing act . . . . . . . . . . . . . 553--561
Anonymous Author Index to Volume 3 . . . . . . . . 563--563
Pieter Hartel and
Rinus Plasmeijer Special Issue on State-of-The-Art
Applications of Pure Functional
Programming languages . . . . . . . . . 565--566
Anonymous JFP volume 3 issue 4 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 3 issue 4 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b3
Kavi Arya A functional animation starter-kit . . . 1--18
John A. Keane An overview of the Flagship system . . . 19--45
Rafael D. Lins and
Simon J. Thompson and
Simon Peyton Jones On the equivalence between CMC and TIM 47--63
F. Warren Burton and
V. J. Rayward-Smith Worst case scheduling for parallel
functional programs . . . . . . . . . . 65--75
Thierry Coquand and
Hugo Herbelin A-translation and looping combinators in
pure type systems . . . . . . . . . . . 77--88
Hong Zhu How powerful are folding/unfolding
transformations? . . . . . . . . . . . . 89--112
Pierre-Louis Curien and
Thér\`ese Hardin Theoretical Pearl: Yet yet a
counterexample for $ \lambda $ +SP . . . 113--115
Lennart Augustsson and
Mikael Rittri and
Dan Synek Functional Pearl: On generating unique
names . . . . . . . . . . . . . . . . . 117--123
Anonymous JFP volume 4 issue 1 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 4 issue 1 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b4
Philip Wadler Type systems for object-oriented
programming . . . . . . . . . . . . . . 125--125
Mitchell Wand Introduction . . . . . . . . . . . . . . 125--126
Kim B. Bruce A paradigmatic object-oriented
programming language: Design, static
typing and semantics . . . . . . . . . . 127--206
Benjamin C. Pierce and
David N. Turner Simple type-theoretic foundations for
object-oriented programming . . . . . . 207--247
Martin Abadi Baby Modula-3 and a theory of objects 249--283
Anonymous JFP volume 4 issue 2 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 4 issue 2 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
Mads Tofte Principal signatures for higher-order
program modules . . . . . . . . . . . . 285--335
Henrik Nilsson and
Peter Fritzson Algorithmic debugging for lazy
functional languages . . . . . . . . . . 337--369
Gérard Huet Residual theory in $ \lambda $-calculus:
a formal development . . . . . . . . . . 371--394
Anonymous JFP volume 4 issue 3 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 4 issue 3 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b3
Ian Mackie Lilac: a functional programming language
based on linear logic . . . . . . . . . 395--433
Fritz Henglein and
Harry G. Mairson The complexity of type inference for
higher-order typed lambda calculi . . . 435--477
Björn Lisper Total unfolding: theory and applications 479--498
Robert Glück On the generation of specializers . . . 499--514
Wei-Ngan Chin Safe fusion of functional expressions
II: Further improvements . . . . . . . . 515--555
Graham Hutton Book Review: \booktitleIntroduction to
HOL: a theorem proving environment for
higher order logic, by Gordon Mike and
Melham Tom (eds.), Cambridge University
Press, 1993, ISBN 0-521-44189-7 . . . . 557--559
Anonymous Author Index to Volume 4 . . . . . . . . 561--561
Anonymous JFP volume 4 issue 4 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 4 issue 4 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
Mark P. Jones A system of constructor classes:
overloading and implicit higher-order
polymorphism . . . . . . . . . . . . . . 1--35
Christine Ernoult and
Alan Mycroft Untyped strictness analysis . . . . . . 37--49
Enrico Tronci Defining data structures via Böhm-out . . 51--64
P. N. Benton Strong normalisation for the linear term
calculus . . . . . . . . . . . . . . . . 65--80
Peter Achten and
Rinus Plasmeijer The ins and outs of Clean I/O . . . . . 81--110
M. Abadi and
L. Cardelli and
B. Pierce and
D. Rémy Dynamic typing in polymorphic languages 111--130
K. Mitchell Book Review: \booktitleAbstract Data
Types in Standard ML, by Rachel
Harrison, John Wiley & Sons, 1993, 212
pp., ISBN 0-471-93844-0 . . . . . . . . 131--134
Anonymous JFP volume 5 issue 1 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 5 issue 1 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
C. Barry Jay and
Neil Ghani The virtues of eta-expansion . . . . . . 135--154
Andrew Tolmach and
Andrew W. Appel A Debugger for Standard ML . . . . . . . 155--200
Tobias Nipkow and
Christian Prehofer Type Reconstruction for Type Classes . . 201--224
Chris Clack and
Stuart Clayman and
David Parrott Lexical profiling: theory and practice 225--277
Anonymous JFP volume 5 issue 2 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 5 issue 2 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b3
Pieter Hartel and
Rinus Plasmeijer Special Issue on State-of-the-art
applications of pure functional
programming languages . . . . . . . . . 279--281
Jeffrey Hammes and
Olaf Lubeck and
Wim Böhm Comparing Id and Haskell in a Monte
Carlo photon transport code . . . . . . 283--316
Donald A. Ziff and
Stephen P. Spackman and
Keith Waclena Funser: a functional server for textual
information retrieval . . . . . . . . . 317--343
Greg Michaelson and
Norman Scaife Prototyping a parallel vision system in
Standard ML . . . . . . . . . . . . . . 345--382
Walter A. C. A. J. De Hoon and
Luc M. W. J. Rutten and
Marko C. J. D. van Eekelen Implementing a functional spreadsheet in
clean . . . . . . . . . . . . . . . . . 383--414
J. R. Davy and
P. M. Dew A polymorphic library for constructive
solid geometry . . . . . . . . . . . . . 415--442
Marcel Turcotte and
Guy Lapalme and
François Major Exploring the conformations of nucleic
acids . . . . . . . . . . . . . . . . . 443--460
Anonymous JFP volume 5 issue 3 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 5 issue 3 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b4
Charles Consel and
Siau Cheng Khoo On-line and off-line partial evaluation:
semantic specifications and correctness
proofs . . . . . . . . . . . . . . . . . 461--500
Amir Kishon and
Paul Hudak Semantics directed program execution
monitoring . . . . . . . . . . . . . . . 501--547
Willem G. Vree and
Pieter H. Hartel Communication lifting: fixed point
computation for parallelism . . . . . . 549--581
Chris Okasaki Simple and efficient purely functional
queues and deques . . . . . . . . . . . 583--592
Martin Hofmann and
Benjamin Pierce A unifying type-theoretic framework for
objects . . . . . . . . . . . . . . . . 593--635
Fairouz Kamareddine and
Rob Nederpelt Refining reduction in the lambda
calculus . . . . . . . . . . . . . . . . 637--651
Luc Duponcheel Book Review: \booktitleConcurrent
Programming in Erlang, by Armstrong Joe,
Virding Robert and Williams Mike,
Prentice Hall, 1993, 281 pp. . . . . . . 653--660
Anonymous Author Index to Volume 5 . . . . . . . . 661--662
Anonymous JFP volume 5 issue 4 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 5 issue 4 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b5
Richard Bird and
Oege De Moor and
Paul Hoogendijk Generic functional programming with
types and relations . . . . . . . . . . 1--28
Pieter H. Hartel and
Hugh Glaser The resource constrained shortest path
problem implemented in a lazy functional
language . . . . . . . . . . . . . . . . 29--46
Andrew W. Appel and
Zhong Shao Empirical and analytic study of stack
versus heap cost for languages with
closures . . . . . . . . . . . . . . . . 47--74
Geoffrey Burn and
Daniel Le Métayer Proving the correctness of compiler
optimisations based on a global
analysis: a study of strictness analysis 75--109
John Greiner Weak polymorphism can be sound . . . . . 111--141
P. W. Grant and
J. A. Sharp and
M. F. Webster and
X. Zhang Sparse matrix representations in a
functional language . . . . . . . . . . 143--170
Peter W. O'Hearn Note on Algol and conservatively
extending functional programming . . . . 171--180
Graham Hutton and
Erik Meijer Functional Pearl: Back to basics:
Deriving representation changers
functionally . . . . . . . . . . . . . . 181--188
Michael Fourman Book Reviews: \booktitleProgramming with
Standard ML, by Myers Colin, Clack Chris
and Poon Ellen, Prentice Hall
International, Inc., New Jersey, 301
pp., 1993, ISBN 0-13-722075-8.
\booktitleML for the Working Programmer,
by Paulson, L. C., Cambridge University
Press, 1991, 429 pp., ISBN
0-521-39022-2. \booktitleElements of ML
Programming, by Ullman, Jeffrey D.,
Prentice Hall International, Inc., New
Jersey, 1994, 320 pp., ISBN
0-13-288788-6, 0-13-184854-2 (USA) . . . 189--193
Anonymous JFP volume 6 issue 1 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 6 issue 1 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b5
Jawahar Chirimar and
Carl A. Gunter and
Jon G. Riecke Reference counting as a computational
interpretation of linear logic . . . . . 195--244
Fairouz Kamareddine and
Rob Nederpelt Canonical typing and $ \Pi $-conversion
in the Barendregt Cube . . . . . . . . . 245--267
Anders Bondorf and
Jens Palsberg Generating action compilers by partial
evaluation . . . . . . . . . . . . . . . 269--298
Pierre-Louis Curien and
Roberto Di Cosmo A confluent reduction for the $ \lambda
$-calculus with surjective pairing and
terminal object . . . . . . . . . . . . 299--327
A. N. Clark Formal basis for the refinement of rule
based transition systems . . . . . . . . 329--354
Andrew Partridge and
David Wright Predictive parser combinators need four
values to report errors . . . . . . . . 355--364
J. J. Leifer and
B. A. Sufrin Functional Pearl Deduction for
functional programmers . . . . . . . . . 365--373
Andrew D. Gordon Book Reviews: \booktitleAn Introduction
to Formal Specification and Z, by Potter
Ben, Sinclair Jane and Till David,
Prentice-Hall, 1991. \booktitleZ: An
Introduction to Formal Methods (second
edition) by Diller Antoni, John Wiley &
Sons, 1994 . . . . . . . . . . . . . . . 375--377
Anonymous JFP volume 6 issue 2 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 6 issue 2 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b3
Bart Jacobs On cubism . . . . . . . . . . . . . . . 379--392
Robert Harper and
Mark Lillibridge Operational interpretations of an
extension of F $ \omega $ with control
operators . . . . . . . . . . . . . . . 393--418
D. B. Carpenter and
H. Glaser Some lattice-based scientific problems,
expressed in Haskell . . . . . . . . . . 419--444
Steve Hill Combinators for parsing expressions . . 445--464
Paul Hudak and
Tom Makucevich and
Syam Gadde and
Bo Whong Haskore music notation --- An algebra of
music . . . . . . . . . . . . . . . . . 465--484
Konstantin Läufer Type classes with existential types . . 485--518
Franco Barbanera and
Stefano Berardi Proof-irrelevance out of excluded-middle
and choice in the calculus of
constructions . . . . . . . . . . . . . 519--526
Andrew J. Kennedy Functional Pearls: Drawing trees . . . . 527--534
Jeremy Gibbons Functional Pearls: Deriving tidy
drawings of trees . . . . . . . . . . . 535--562
Anonymous JFP volume 6 issue 3 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 6 issue 3 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
John Launchbury and
Gebreselassie Baraki Representing demand by partial
projections . . . . . . . . . . . . . . 563--585
Colin Runciman and
Niklas Röjemo New dimensions in heap profiling . . . . 587--620
Pieter H. Hartel and
Marc Feeley and
Martin Alt and
Lennart Augustsson and
Peter Baumann and
Marcel Beemster and
Emmanuel Chailloux and
Christine H. Flood and
Wolfgang Grieskamp and
John H. G. Van Groningen and
Kevin Hammond and
Bogumil Hausman and
Melody Y. Ivory and
Richard E. Jones and
Jasper Kamperman and
Peter Lee and
Xavier Leroy and
Rafael D. Lins and
Sandra Loosemore and
Niklas Röjemo and
Manuel Serrano and
Jean-Pierre Talpin and
Jon Thackray and
Stephen Thomas and
Pum Walters and
Pierre Weis and
Peter Wentworth Benchmarking implementations of
functional languages with `Pseudoknot',
a float-intensive benchmark . . . . . . 621--655
Jeremy Gibbons Functional Pearls: The Third
Homomorphism Theorem . . . . . . . . . . 657--665
Anonymous JFP volume 6 issue 4 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 6 issue 4 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b3
Xavier Leroy A syntactic theory of type generativity
and sharing . . . . . . . . . . . . . . 667--698
Zine-El-Abidine Benaissa and
Daniel Briaud and
Pierre Lescanne and
Jocelyne Rouyer-Degli $ \lambda \nu $, a calculus of explicit
substitutions which preserves strong
normalisation . . . . . . . . . . . . . 699--722
Dietmar Gärtner and
Werner E. Kluge $ \pi $-RED + An interactive compiling
graph reduction system for an applied $
\lambda $-calculus . . . . . . . . . . . 723--756
Marc Bezem and
Jan Springintveld A simple proof of the undecidability of
inhabitation in $ \lambda $P . . . . . . 757--761
Anonymous JFP volume 6 issue 5 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 6 issue 5 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b3
Andrea Asperti and
Cecilia Giovannetti and
Andrea Naletto The Bologna optimal higher-order machine 763--810
M. H. Sòrensen and
R. Glück and
N. D. Jones A positive supercompiler . . . . . . . . 811--838
Gerth Stòlting Brodal and
Chris Okasaki Optimal purely functional priority
queues . . . . . . . . . . . . . . . . . 839--857
Anonymous Author Index to Volume 6 . . . . . . . . 859--861
Anonymous JFP volume 6 issue 6 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 6 issue 6 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b3
Gul A. Agha and
Ian A. Mason and
Scott F. Smith and
Carolyn L. Talcott A foundation for actor computation . . . 1--72
P. Rondogiannis and
W. W. Wadge First-order functional languages and
intensional logic . . . . . . . . . . . 73--101
J. Hammes and
S. Sur and
W. Böhm On the effectiveness of functional
language features: NAS benchmark FT . . 103--123
Tom Melham Call for Papers: \booktitleJournal of
Functional Programming Special Issue on
Theorem Provers and Functional
Programming . . . . . . . . . . . . . . 125--126
Philip Wadler EDITORIAL: A HOT opportunity . . . . . . 127--128
Tetsuo Ida and
Koichi Nakahara Leftmost outside-in narrowing calculi 129--161
Nigel W. O. Hutchison and
Ute Neuhaus and
Manfred Schmidt-Schauss and
Cordy V. Hall \sc Natural Expert: a commercial
functional programming environment . . . 163--182
Owen Kaser and
C. R. Ramakrishnan and
I. V. Ramakrishnan and
R. C. Sekar \sc Equals --- a fast parallel
implementation of a lazy language . . . 183--217
Colin Runciman Functional Pearl: Lazy wheel sieves and
spirals of primes . . . . . . . . . . . 219--225
Andrew W. Appel Book Review: \booktitleGarbage
Collection: Algorithms for Automatic
Dynamic Memory Management, by Richard
Jones and Rafael Lins, John Wiley & Sons,
1996 . . . . . . . . . . . . . . . . . . 227--229
Peter Sestoft Deriving a lazy abstract machine . . . . 231--264
Zena M. Ariola and
Matthias Felleisen The call-by-need lambda calculus . . . . 265--301
John Hatcliff and
Olivier Danvy Thunks and the $ \lambda $-calculus . . 303--319
Torben Amtoft and
Flemming Nielson and
Hanne Riis Nielson Type and behaviour reconstruction for
higher-order concurrent programs . . . . 321--347
Richard S. Bird Functional Pearl: On merging and
selection . . . . . . . . . . . . . . . 349--354
Harry Mairson and
Bruce Kapron Call for Papers: \booktitleJournal of
Functional Programming Special Issue on
Functional Programming and Computational
Complexity . . . . . . . . . . . . . . . 355--356
Tyng-Ruey Chuang and
Benjamin Goldberg A syntactic method for finding least
fixed points of higher-order functions
over finite domains . . . . . . . . . . 357--394
Fairouz Kamareddine and
Alejandro Ríos Extending a $ \lambda $-calculus with
explicit substitution which preserves
strong normalisation into a confluent
calculus on open terms . . . . . . . . . 395--420
Gad Aharoni and
Amnon Barak and
Amir Ronen A competitive algorithm for managing
sharing in the distributed execution of
functional programs . . . . . . . . . . 421--440
Richard S. Bird Functional Pearl: On building trees with
minimum height . . . . . . . . . . . . . 441--445
Chris Reade Book Reviews: \booktitleML for the
Working Programmer (2nd edition) by L.
C. Paulson, Cambridge University Press,
1996. \booktitleA Practical Course in
Functional Programming Using Standard
ML, by R. Bosworth, McGraw Hill, 1996 447--449
Reinhold Heckmann and
Reinhard Wilhelm A functional description of \TeX's
formula layout . . . . . . . . . . . . . 451--485
Melissa E. O'Neill and
F. Warren Burton A new method for functional arrays . . . 487--513
Andrew W. Appel and
Trevor Jim Shrinking lambda expressions in linear
time . . . . . . . . . . . . . . . . . . 515--540
Richard Bird and
Geraint Jones and
Oege De Moor More haste, less speed: lazy versus
eager evaluation . . . . . . . . . . . . 541--547
Gérard Huet The Zipper . . . . . . . . . . . . . . . 549--554
Rex Page Book Review: \booktitleApplications of
Functional Programming, by Colin
Runciman and David Wakeling, editors,
UCL Press, 1995 . . . . . . . . . . . . 555--556
P. Òrbæk and
J. Palsberg Trust in the $ \lambda $-calculus . . . 557--591
Sabine Broda and
Luís Damas On combinatory complete sets of proper
combinators . . . . . . . . . . . . . . 593--612
Franco Barbanera and
Maribel Fernández and
Herman Geuvers Modularity of strong normalization in
the algebraic-$ \lambda $-cube . . . . . 613--660
Chris Okasaki Three algorithms on Braun trees . . . . 661--666
R. D. Tennent Book Review: \booktitleFoundations for
Programming Languages, by John C.
Mitchell, MIT Press, 1996 . . . . . . . 667--668
Amr Sabry What is a purely functional language? 1--22
P. W. Trinder and
K. Hammond and
H.-W. Loidl and
S. L. Peyton Jones Algorithm + strategy = parallelism . . . 23--60
David Wakeling The dynamic compilation of lazy
functional programs . . . . . . . . . . 61--81
Richard S. Bird Meertens number . . . . . . . . . . . . 83--88
Erik Poll Expansion postponement for normalising
pure type systems . . . . . . . . . . . 89--96
Robert F. Stärk Why the constant `undefined'? Logics of
partial terms for strict and non-strict
functional programming languages . . . . 97--129
Thér\`ese Hardin and
Luc Maranget and
Bruno Pagano Functional runtime systems within the
lambda-sigma calculus . . . . . . . . . 131--176
P. N. Benton and
G. M. Bierman and
V. C. V. De Paiva Computational types from a logical
perspective . . . . . . . . . . . . . . 177--193
Chris Okasaki Even higher-order functions for parsing
or Why would anyone ever want to use a
sixth-order function? . . . . . . . . . 195--199
R. G. Morgan and
S. A. Jarvis Profiling large-scale lazy functional
programs . . . . . . . . . . . . . . . . 201--237
John Hannan A type-based escape analysis for
functional languages . . . . . . . . . . 239--273
John Maraist and
Martin Odersky and
Philip Wadler The call-by-need lambda calculus . . . . 275--317
Simon Peyton Jones and
Phil Wadler EDITORIAL . . . . . . . . . . . . . . . 319--321
Thomas Johnsson Efficient graph algorithms using lazy
monolithic arrays . . . . . . . . . . . 323--333
Furio Honsell and
Alberto Pravato and
Simona Ronchi Della Rocca Structured Operational Semantics of a
fragment of the language Scheme . . . . 335--365
Andrew Tolmach and
Dino P. Oliva From ML to Ada: Strongly-typed language
interoperability via source translation 367--412
Michael Hedberg A coherence theorem for Martin-Löf's type
theory . . . . . . . . . . . . . . . . . 413--436
Graham Hutton and
Erik Meijer Monadic parsing in Haskell . . . . . . . 437--444
Rex Page Book Review: \booktitleApplications of
Functional Programming edited by Colin
Runciman and David Wakeling, UCL Press
Limited, 1995 . . . . . . . . . . . . . 445--446
William Ferreira and
Matthew Hennessy and
Alan Jeffrey A theory of weak bisimulation for Core
CML . . . . . . . . . . . . . . . . . . 447--491
Guy Lapalme Dynamic tabbing for automatic
indentation with the layout rule . . . . 493--502
Gary Meehan and
Mike Joy Animated fuzzy logic . . . . . . . . . . 503--525
Patrik Jansson and
Johan Jeuring Polytypic unification . . . . . . . . . 527--536
Alan Jeffrey Book Review: \booktitleML with
Concurrency, by Flemming Nielson (ed.),
Springer-Verlag, 1997 . . . . . . . . . 537--542
Th. Streicher and
B. Reus Classical logic, continuation semantics
and abstract machines . . . . . . . . . 543--572
C. B. Jay and
G. Bell\`e and
E. Moggi Functorial ML . . . . . . . . . . . . . 573--619
Olivier Danvy Functional unparsing . . . . . . . . . . 621--625
Martin Erwig Diets for fat sets . . . . . . . . . . . 627--632
Hamilton Richards Book Reviews: \booktitleHaskell: The
Craft of Functional Programming, by
Simon Thompson, Addison--Wesley, 1996.
\booktitleMiranda 81: The Craft of
Functional Programming, by Simon
Thompson, Addison--Wesley, 1995 . . . . 633--637
Stefan Kahrs Book Review: \booktitleHigher Order
Operational Techniques in Semantics
edited by Andrew D. Gordon and Andrew M.
Pitts, Cambridge University Press 1998,
ISBN 0-521-63168-8 (hardback) . . . . . 633--637
C. Flanagan and
M. Felleisen The semantics of future and an
application . . . . . . . . . . . . . . 1--31
Michael Hanus and
Christian Prehofer Higher-order narrowing with definitional
trees . . . . . . . . . . . . . . . . . 33--75
Richard S. Bird and
Ross Paterson de Bruijn notation as a nested datatype 77--91
Ralf Hinze Explaining binomial heaps . . . . . . . 93--104
Bruce McKenzie Book Review: \booktitleModern Compiler
Implementation in ML: Basic Techniques,
by Andrew W. Appel, Cambridge University
Press, 1997, ISBN 0-521-58775-1 . . . . 105--111
Simon Thompson Book Review: \booktitleAdvanced
Functional Programming, edited by John
Lauchbury, Erik Meijer and Tim Sheard,
Lecture Notes in Computer Science 1129,
Springer-Verlag, 1996 . . . . . . . . . 105--111
F. Warren Burton Book Review: \booktitleAdvanced
Functional Programming: Lecture Notes in
Computer Science 925, edited by Johan
Jeuring and Erik Meijer,
Springer-Verlag, 1995 . . . . . . . . . 105--111
Richard J. Boulton Transparent optimisation of rewriting
combinators . . . . . . . . . . . . . . 113--146
Keith Hanna Implementing theorem provers in a purely
functional style . . . . . . . . . . . . 147--166
C. Lüth and
B. Wolff Functional design and implementation of
graphical user interfaces for theorem
provers . . . . . . . . . . . . . . . . 167--189
Olaf Müller and
Tobias Nipkow and
David Von Oheimb and
Oscar Slotosch HOLCF = HOL + LCF . . . . . . . . . . . 191--223
Andrew Ireland and
Alan Bundy Automatic verification of functions with
accumulating parameters . . . . . . . . 225--245
Martin Hofmann Semantics of linear/modal lambda
calculus . . . . . . . . . . . . . . . . 247--277
Christoph A. Herrmann and
Christian Lengauer Parallelization of divide-and-conquer by
translation to nested loops . . . . . . 279--310
Richard Bird Editorial . . . . . . . . . . . . . . . 311--311
Koen Claessen A poor man's concurrency monad . . . . . 313--323
M. Douglas Mcilroy Power series, power serious . . . . . . 325--337
Jeremy Gibbons A pointless derivation of radix sort . . 339--346
Paul A. Bailes Book Review: \booktitleFunctional
Programming Languages in Education, by
P. H. Hartel and R. Plasmeijer, editors,
Springer-Verlag, 1995 . . . . . . . . . 347--354
Erik Poll and
Simon Thompson Book Review: \booktitleAlgebra of
Programming, by Richard Bird and Oege de
Moor, Prentice Hall, 1996 (dated 1997) 347--354
Graham Hutton A tutorial on the universality and
expressiveness of fold . . . . . . . . . 355--372
Andrew D. Gordon and
Paul D. Hankin and
Sòren B. Lassen Compilation and equivalence of
imperative objects . . . . . . . . . . . 373--426
Susumu Nishimura and
Atsushi Ohori Parallel functional programming on
recursively defined data via
data-parallel recursion . . . . . . . . 427--462
Robert Harper Proof-directed debugging . . . . . . . . 463--469
Chris Okasaki Red-black trees in a functional setting 471--477
Pieter Hartel Book Review: \booktitleThe Functional
Approach to Programming, by Guy
Cousineau and Michel Mauny, Cambridge
University Press, 1998, ISBN
0-521-57681-4 pbk, xiv+445 pp. . . . . . 479--482
Chris Okasaki Book Review: \booktitleComputability and
Complexity: From a Programming
Perspective, by Neil D. Jones, MIT
Press, 1997 . . . . . . . . . . . . . . 479--482
Peter Thiemann Combinators for program generation . . . 483--525
P. Rondogiannis and
W. W. Wadge Higher-order functional languages and
intensional logic . . . . . . . . . . . 527--564
Richard Statman and
Henk Barendregt Applications of Plotkin-terms:
partitions and morphisms for closed
terms . . . . . . . . . . . . . . . . . 565--575
Ralf Hinze Book Review: \booktitlePurely Functional
Data Structures, by Chris Okasaki,
Cambridge University Press, 1998, 220
pp. . . . . . . . . . . . . . . . . . . 577--578
David Wakeling Compiling lazy functional programs for
the Java Virtual Machine . . . . . . . . 579--603
Dinh Lê and
D. Stott Parker Using randomization to make recursive
matrix algorithms practical . . . . . . 605--624
Tristan Crolard A confluent $ \lambda $-calculus with a
catch/throw mechanism . . . . . . . . . 625--647
Alfons Geser and
Sergei Gorlatch Parallelizing functional programs by
generalization . . . . . . . . . . . . . 649--673
Gilles Barthe Type-checking injective pure type
systems . . . . . . . . . . . . . . . . 675--698
Erik Meijer Server side web scripting in Haskell . . 1--18
Limsoon Wong Kleisli, a functional query system . . . 19--56
Yang Jung and
Greg Michaelson A visualisation of polymorphic type
checking . . . . . . . . . . . . . . . . 57--75
Masahito Hasegawa Girard translation and logical
predicates . . . . . . . . . . . . . . . 77--89
Mark Hayden Distributed communication in ML . . . . 91--120
Henk Barendregt and
Silvia Ghilezan Lambda terms for natural deduction,
sequent calculus and cut elimination . . 121--134
Joëlle Despeyroux and
Robert Harper Special issue on Logical Frameworks and
Metalanguages . . . . . . . . . . . . . 135--136
Gustavo Betarte Type checking dependent (record) types
and subtyping . . . . . . . . . . . . . 137--166
G. M. Bierman Program equivalence in a linear
functional language . . . . . . . . . . 167--190
Paul Hoogendijk and
Oege De Moor Container types categorically . . . . . 191--225
Nikolaos S. Papaspyrou and
Dragan Ma\'cos A study of evaluation order semantics in
expressions with side effects . . . . . 227--244
Simon Thompson A functional reactive animation of a
lift using Fran . . . . . . . . . . . . 245--268
Xavier Leroy A modular module system . . . . . . . . 269--303
Ralf Hinze Perfect trees and bit-reversal
permutations . . . . . . . . . . . . . . 305--317
Graham Hutton Special issue on Haskell . . . . . . . . 319--319
Bruno Guillaume The $ \lambda s_e$-calculus does not
preserve strong normalisation . . . . . 321--325
Ralf Hinze Generalizing generalized tries . . . . . 327--351
Manuel Serrano Bee: an integrated development
environment for the Scheme programming
language . . . . . . . . . . . . . . . . 353--395
Michael Spivey Combinators for breadth-first search . . 397--408
Daniel Fridlender and
Mia Indrika Do we need dependent types? . . . . . . 409--415
Gilles Barthe and
Morten Heine Sòrensen Domain-free pure type systems . . . . . 417--452
Joachim Niehren Uniform confluence in concurrent
computation . . . . . . . . . . . . . . 453--499
R. D. Tennent Book Review: \booktitleTheories of
Programming Languages, by John C.
Reynolds, Cambridge University Press,
1998 . . . . . . . . . . . . . . . . . . 501--508
Björn von Sydow Book Review: \booktitleThe Haskell
School of Expression: Learning
Functional Programming Through
Multimedia, by Paul Hudak, Cambridge
University Press, 2000, 363 pp., ISBN
0-521-64408-9 . . . . . . . . . . . . . 501--508
Greg Michaelson Book Review: \booktitleThe Optimal
Implementation of Functional Programming
Languages, by A. Asperti and S.
Guerrini, Cambridge University Press,
1998, 392 pp. . . . . . . . . . . . . . 501--508
Rafael D. Lins Book Review: \booktitleResearch
Directions in Parallel Functional
Programming, by Kevin Hammond and Greg
Michaelson, editors, Springer-Verlag,
1999 . . . . . . . . . . . . . . . . . . 501--508
Ferruccio Damiani and
Paola Giannini Automatic useless-code elimination for
HOT functional programs . . . . . . . . 509--559
Pascal Fradet and
Julien Mallet Compilation of a specialized functional
language for massively parallel
computers . . . . . . . . . . . . . . . 561--605
Mayer Goldberg An adequate and efficient
left-associated binary numeral system in
the $ \lambda $-calculus . . . . . . . . 607--623
Walid Taha and
Peter Wadler Special issue on Semantics,
Applications, and Implementation of
Program Generation . . . . . . . . . . . 627--627
Daniel Leivant and
Bob Constable Editorial . . . . . . . . . . . . . . . 1--1
Ralph Benzinger Automated complexity analysis of Nuprl
extracted programs . . . . . . . . . . . 3--31
G. Bonfante and
A. Cichon and
J.-Y. Marion and
H. Touzet Algorithms with polynomial
interpretation termination proof . . . . 33--53
Neil D. Jones The expressive power of higher-order
types or, life without CONS . . . . . . 55--94
Salvatore Caporaso and
Emanuele Covino and
Giovanni Pani A predicative approach to the
classification problem . . . . . . . . . 95--116
Robert J. Irwin and
James S. Royer and
Bruce M. Kapron On characterizations of the basic
feasible functionals, Part I . . . . . . 117--153
Margaret Burnett and
John Atwood and
Rebecca Walpole Djang and
James Reichwein and
Herkimer Gottfried and
Sherry Yang Forms/3: A first-order visual language
to explore the boundaries of the
spreadsheet paradigm . . . . . . . . . . 155--206
Hél\`ene Kirchner and
Pierre-Etienne Moreau Promoting rewriting to a programming
language: a compiler for
non-deterministic rewrite programs in
associative-commutative theories . . . . 207--251
Alan Wood Book Review: \booktitleStructure and
Interpretation of Computer Programs, 2nd
Ed by Abelson and Sussman, with Sussman,
MIT Press, 1996, ISBN 0-262-51087-1, 657
pp. . . . . . . . . . . . . . . . . . . 253--262
John O'Donnell Book Review: \booktitleConcurrent
Programming in ML, by John H. Reppy,
Cambridge University Press, 1999, ISBN
0-521-48089-2, xv+308 pp. . . . . . . . 253--262
Jan Willem Klop Book Review: \booktitleTerm Rewriting
and All That, by Franz Baader and Tobias
Nipkow, Cambridge University Press,
1998, ISBN 0-521-45520-0 (hardback), 301
pp. . . . . . . . . . . . . . . . . . . 253--262
Michael Hanus Book Review: \booktitleProgramming with
Constraints: An Introduction, by Kim
Marriott and Peter J. Stuckey, MIT
Press, 1998 . . . . . . . . . . . . . . 253--262
Werner Kluge Book Review: \booktitleIntroduction to
Programming Using SML, by M. R. Hansen
and H. Rischel, Addison Wesley, 1999,
ISBN 0-201-39820-6 . . . . . . . . . . . 253--262
Jens Palsberg and
Christina Pavlopoulou From Polyvariant flow information to
intersection and union types . . . . . . 263--317
Mitchell Wand and
William D. Clinger Set constraints for destructive array
update optimization . . . . . . . . . . 319--346
Richard S. Bird Functional Pearl: Unfolding pointer
algorithms . . . . . . . . . . . . . . . 347--358
Andrew J. Bennett and
Paul H. J. Kelly and
Ross A. Paterson Pipelined functional tree accesses and
updates: scheduling, synchronization,
caching and coherence . . . . . . . . . 359--393
Nick Benton and
Andrew Kennedy Exceptional syntax . . . . . . . . . . . 395--410
Richard S. Bird Maximum marking problems . . . . . . . . 411--424
Stefan Kahrs Red-black trees with types . . . . . . . 425--432
Roy Dyckhoff Book Review: \booktitleComputational
Logic, by Ulrich Berger and Helmut
Schwichtenberg, editors,
Springer-Verlag, 1999, 444 pp. . . . . . 433--436
Alan Jeffrey Book Review: \booktitleCommunicating and
Mobile Systems: the $ \pi $-calculus, by
Robin Milner, Cambridge University
Press, 1999 . . . . . . . . . . . . . . 433--436
Gilles Barthe and
Peter Dybjer and
Peter Thiemann Special issue on Dependent Type Theory
Meets Programming Practice: Call for
papers . . . . . . . . . . . . . . . . . 437--437
Chris Okasaki Special issue on Algorithmic aspects of
functional programming languages . . . . 439--440
Guy Blelloch and
Hal Burch and
Karl Crary and
Robert Harper and
Gary Miller and
Noel Walkington Persistent triangulations . . . . . . . 441--466
Martin Erwig Inductive graphs and functional graph
algorithms . . . . . . . . . . . . . . . 467--492
Ralf Hinze Manufacturing datatypes . . . . . . . . 493--524
Graeme E. Moss and
Colin Runciman Inductive benchmarking for purely
functional data structures . . . . . . . 525--556
Thomas Nordin and
Andrew Tolmach Modular lazy search for Constraint
Satisfaction Problems . . . . . . . . . 557--587
Valeria de Paiva Book Review: \booktitleDomains and
Lambda-Calculi, by R. M. Amadio and
P.-L. Curien, Springer-Verlag, 1999,
ISBN 0-521-58775-1 . . . . . . . . . . . 589--589
E. Moggi and
Amr Sabry Monadic encapsulation of effects: a
revised approach (extended version) . . 591--627
Henrik Nilsson How to look busy while being as lazy as
ever: the Implementation of a lazy
functional debugger . . . . . . . . . . 629--671
Olivier Danvy and
Morten Rhiger and
Kristoffer H. Rose Normalization by evaluation with typed
abstract syntax . . . . . . . . . . . . 673--680
Ralf Hinze and
Johan Jeuring Weaving a web . . . . . . . . . . . . . 681--689
Andreas Abel and
Thorsten Altenkirch A predicative analysis of structural
recursion . . . . . . . . . . . . . . . 1--41
Greg Morrisett and
Karl Crary and
Neal Glew and
David Walker Stack-based typed assembly language . . 43--88
Mike Thomas Book Review: \booktitlePrinciples of
Programming Languages Design,
Evaluation, and Implementation (3rd
ed.), by Bruce J. MacLennan, Oxford
University Press, 1999, ISBN
0-19-511306-3 . . . . . . . . . . . . . 89--90
Davide Ancona and
Elena Zucca A calculus of module systems . . . . . . 91--132
Dominic Duggan and
John Ophel Type-checking multi-parameter type
classes . . . . . . . . . . . . . . . . 133--158
Robert Bruce Findler and
John Clements and
Cormac Flanagan and
Matthew Flatt and
Shriram Krishnamurthi and
Paul Steckler and
Matthias Felleisen DrScheme: a programming environment for
Scheme . . . . . . . . . . . . . . . . . 159--182
J. B. Wells and
Allyn Dimock and
Robert Muller and
Franklyn Turbak A calculus with polymorphic and
polyvariant flow types . . . . . . . . . 183--227
Silvano Dal Zilio and
Andrew D. Gordon Region analysis and a $ \pi $-calculus
with groups . . . . . . . . . . . . . . 229--292
Graham Hutton Special Double Issue on Haskell . . . . 293--294
Karl-Filip Faxén A static semantics for Haskell . . . . . 295--357
Simon Marlow Developing a high-performance web server
in Concurrent Haskell . . . . . . . . . 359--374
Conor McBride Faking it Simulating dependent types in
Haskell . . . . . . . . . . . . . . . . 375--392
Simon Peyton Jones and
Simon Marlow Secrets of the Glasgow Haskell Compiler
inliner . . . . . . . . . . . . . . . . 393--434
Peter Thiemann A typed representation for HTML and XML
documents in Haskell . . . . . . . . . . 435--468
P. W. Trinder and
H.-W. Loidl and
R. F. Pointon Parallel and Distributed Haskells . . . 469--510
Vladimir Gapeyev and
Michael Y. Levin and
Benjamin C. Pierce Recursive subtyping revealed . . . . . . 511--548
Peter Selinger The lambda calculus is algebraic . . . . 549--566
Karl Crary and
Stephanie Weirich and
Greg Morrisett Intensional polymorphism in type-erasure
semantics . . . . . . . . . . . . . . . 567--600
Ralf Hinze A fresh look at binary search trees . . 601--607
Graham Hutton The countdown problem . . . . . . . . . 609--616
Daniel P. Friedman and
Amr Sabry CPS in little pieces: composing partial
continuations . . . . . . . . . . . . . 617--622
Simon Peyton Jones 1 Introduction . . . . . . . . . . . . . i-6
Simon Peyton Jones 2 Lexical Structure . . . . . . . . . . 7--16
Simon Peyton Jones 3 Expressions . . . . . . . . . . . . . 17--38
Simon Peyton Jones 4 Declarations and Bindings . . . . . . 39--66
Simon Peyton Jones 5 Modules . . . . . . . . . . . . . . . 67--80
Simon Peyton Jones 6 Predefined Types and Classes . . . . . 81--96
Simon Peyton Jones 7 Basic Input/Output . . . . . . . . . . 97--102
Simon Peyton Jones 8 Standard Prelude . . . . . . . . . . . 103--124
Simon Peyton Jones 9 Syntax Reference . . . . . . . . . . . 125--138
Simon Peyton Jones 10 Specification of Derived Instances 139--144
Simon Peyton Jones 11 Compiler Pragmas . . . . . . . . . . 145--146
Simon Peyton Jones 12 Rational Numbers . . . . . . . . . . 149--152
Simon Peyton Jones 13 Complex Numbers . . . . . . . . . . . 153--156
Simon Peyton Jones 14 Numeric Functions . . . . . . . . . . 157--168
Simon Peyton Jones 15 Indexing Operations . . . . . . . . . 169--172
Simon Peyton Jones 16 Arrays . . . . . . . . . . . . . . . 173--178
Simon Peyton Jones 17 List Utilities . . . . . . . . . . . 179--190
Simon Peyton Jones 18 Maybe Utilities . . . . . . . . . . . 191--192
Simon Peyton Jones 19 Character Utilities . . . . . . . . . 193--198
Simon Peyton Jones 20 Monad Utilities . . . . . . . . . . . 199--204
Simon Peyton Jones 21 Input/Output . . . . . . . . . . . . 205--218
Simon Peyton Jones 22 Directory Functions . . . . . . . . . 219--222
Simon Peyton Jones 23 System Functions . . . . . . . . . . 223--224
Simon Peyton Jones 24 Dates and Times . . . . . . . . . . . 225--230
Simon Peyton Jones 25 Locales . . . . . . . . . . . . . . . 231--232
Simon Peyton Jones 26 CPU Time . . . . . . . . . . . . . . 233--234
Simon Peyton Jones 27 Random Numbers . . . . . . . . . . . 235--240
Simon Peyton Jones Bibliography . . . . . . . . . . . . . . 241--255
Gérard Huet Special issue on `Logical frameworks and
metalanguages' . . . . . . . . . . . . . 257--260
Gilles Barthe and
Venanzio Capretta and
Olivier Pons Setoids in type theory . . . . . . . . . 261--293
Michael Y. Levin and
Benjamin C. Pierce TinkerType: a language for playing with
formal systems . . . . . . . . . . . . . 295--316
Zhaohui Luo PAL+: a lambda-free logical framework 317--338
Daria Walukiewicz-Chrzaszcz Termination of rewriting in the Calculus
of Constructions . . . . . . . . . . . . 339--414
Christine Röckl and
Daniel Hirschkoff A fully adequate shallow embedding of
the $ \pi $-calculus in Isabelle/HOL
with mechanized syntax analysis . . . . 415--451
Walid Taha `Semantics, Applications, and
Implementation of Program Generation' 453--454
Conal Elliott and
Sigbjòrn Finne and
Oege De Moor Compiling embedded languages . . . . . . 455--481
Bernd Fischer and
Johann Schumann AutoBayes: a system for generating data
analysis programs from statistical
models . . . . . . . . . . . . . . . . . 483--508
Adam Fischbach and
John Hannan Specification and correctness of lambda
lifting . . . . . . . . . . . . . . . . 509--543
C. Calcagno and
E. Moggi and
T. Sheard Closed types for a safe imperative
MetaML . . . . . . . . . . . . . . . . . 545--571
Peter Thiemann Program specialization for execution
monitoring . . . . . . . . . . . . . . . 573--600
Norman Ramsey Pragmatic aspects of reusable program
generators . . . . . . . . . . . . . . . 601--646
Stefan Monnier and
Zhong Shao Inlining as staged computation . . . . . 647--676
Frederick Smith and
Dan Grossman and
Greg Morrisett and
Luke Hornof and
Trevor Jim Compiling for template-based run-time
code generation . . . . . . . . . . . . 677--708
Jean-Christophe Filliâtre Verification of non-functional programs
using interpretations in type theory . . 709--745
Peter O'Hearn On bunched typing . . . . . . . . . . . 747--796
Patricia Johann Short cut fusion is correct . . . . . . 797--814
Chris Okasaki Theoretical Pearls: Flattening
combinators: surviving without
parentheses . . . . . . . . . . . . . . 815--822
Chris Angus Book Review: \booktitleTrends in
Functional Programming (volumes 1 & 2) by
Greg Michaelson, Phil Trinder and
Hans-Wolfgang Loidl (editors volume 1),
and Stephen Gilmore (editor volume 2).
Intellect Books, Bristol, 2001, 2002 . . 823--824
Gaétan Hains Book Review: \booktitleImplicit parallel
programming in pH, by R. S. Nikhil and
Arvind, Morgan Kaufmann, 2001 . . . . . 824--826
Jerzy Karczmarczuk Book Review: \booktitleStructure and
Interpretation of Classical Mechanics,
by Gerald Jay Sussman and Jack Wisdom
with Meinhard E. Mayer, The MIT Press;
2001, ISBN 0-262-19455-4 . . . . . . . . 826--828
D. Russell Book Review: \booktitleAlgorithms: A
Functional Programming Approach, by
Fethi Rabhi and Guy Lapalme,
Addison--Wesley, 1999, ISBN
0-201-59604-0, xi + 235 pp. . . . . . . 828--829
Walid Taha Book Review: \booktitleEssentials of
Programming Languages (2nd ed), by
Daniel P. Friedman, Mitchell Wand and
Christopher T. Haynes, MIT Press, ISBN
0-262-06217-8, 2001 . . . . . . . . . . 829--831
Bryn Keller Book Review: \booktitleThe World of
Scripting Languages, by David W. Barron,
John Wiley & Sons, 2000, ISBN
0-471-99886-9 . . . . . . . . . . . . . 831--832
Simon Peyton Jones and
Phil Wadler The Educational Pearls column . . . . . 833--834
Matthias Felleisen Welcome to the Educational Pearls Column 835--838
Erick Gallesio and
Manuel Serrano Programming graphical user interfaces
with Scheme . . . . . . . . . . . . . . 839--866
Daniel Damian and
Olivier Danvy Syntactic accidents in program analysis:
on the impact of the CPS transformation 867--904
Jens Palsberg and
Mitchell Wand CPS transformation of flow information 905--923
Daniel Damian and
Olivier Danvy CPS transformation of flow information,
Part II: administrative reductions . . . 925--933
Ralf Hinze Formatting: a class act . . . . . . . . 935--944
Jean-Christophe Filliâtre and
François Pottier Producing all ideals of a forest,
functionally . . . . . . . . . . . . . . 945--956
Greg Morrisett and
Karl Crary and
Neal Glew and
David Walker Stack-based typed assembly language . . 957--959
Haruo Hosoya and
Benjamin C. Pierce Regular expression pattern matching for
XML . . . . . . . . . . . . . . . . . . 961--1004
Sven-Bodo Scholz Single Assignment C: efficient support
for high-level array operations in a
functional setting . . . . . . . . . . . 1005--1059
Conor Mcbride First-order unification by structural
recursion . . . . . . . . . . . . . . . 1061--1075
Christoph Lüth Haskell in Space: An interactive game as
a functional programming exercise . . . 1077--1085
Eerke Boiten Book Review: \booktitleConcepts in
Programming Languages, by John C.
Mitchell, Cambridge University Press,
2002, ISBN 0-521-78098-5 . . . . . . . . 1087--1088
Gilles Barthe and
Peter Dybjen and
Peter Thiemann Introduction to the Special Issue on
Dependent Type Theory Meets Practical
Programming . . . . . . . . . . . . . . 1--2
Andrew W. Appel and
Amy P. Felty Dependent types ensure partial
correctness of theorem provers . . . . . 3--19
Christoph Kreitz Building reliable, high-performance
networks with the Nuprl proof
development system . . . . . . . . . . . 21--68
Conor Mcbride and
James Mckinna The view from the left . . . . . . . . . 69--111
Manuel M. T. Chakravarty and
Gabriele Keller The risks and benefits of teaching
purely functional programming in first
year . . . . . . . . . . . . . . . . . . 113--123
Chris Reade Book Review: \booktitleProof, Language
and Interaction, Essays in Honour of
Robin Milner, eds. Gordon Plotkin, Colin
Sterling, Mads Tofte, Foundations of
Computing Series, MIT Press 2000 . . . . 125--128
Pieter Hartel and
Henk Muller and
Hugh Glaser The Functional ``C'' experience . . . . 129--135
Aarne Ranta Grammatical Framework . . . . . . . . . 145--189
Clem Baker-Finch and
Kevin Glynn and
Simon Peyton Jones Constructed product result analysis for
Haskell . . . . . . . . . . . . . . . . 211--245
Mike Thomas Book Review: \booktitleAn Introduction
to Computing with Haskell, by Manuel M.
T. Chakravarty and Gabrielle C. Keller,
Pearson SprintPrint, 2002, ISBN
1-74009-404-2. Price \$AU 39.95, Pp.
150} . . . . . . . . . . . . . . . . . . 247--249
Eugene Wallingford Book Review: \booktitlePractical Aspects
of Declarative Languages, by Shriram
Krishnamurthi and C. R. Ramakrishnan
(eds.), LNCS 2257, Springer-Verlag,
2002. ISBN 3-540-43092-X Price \pounds
31.50, pp. 359 . . . . . . . . . . . . . 249--251
Martin Erwig Escape from Zurg: an exercise in logic
programming . . . . . . . . . . . . . . 253--261
Gérard Boudol The recursive record semantics of
objects revisited . . . . . . . . . . . 263--315
Janis Voigtländer and
Armin Kühnemann Composition of functions with
accumulating parameters . . . . . . . . 317--363
Paul Hudak and
Greg Morrisett Editorial . . . . . . . . . . . . . . . i--ii
Matthias Felleisen and
Robert Bruce Findler and
Matthew Flatt and
Shriram Krishnamurthi The structure and interpretation of the
computer science curriculum . . . . . . 365--378
Jürgen Giesl and
Aart Middeldorp Transformation techniques for
context-sensitive rewrite systems . . . 379--427
Brian Mcnamara and
Yannis Smaragdakis Functional programming with the FC++
library . . . . . . . . . . . . . . . . 429--472
Anonymous Special issue on ``Programming Language
Technologies for XML'' . . . . . . . . . 473--473
Timothy J. Hickey Computer literacy via Scheme and web
programming . . . . . . . . . . . . . . 475--488
John Hughes Global variables in Haskell . . . . . . 489--502
M. Douglas McIlroy Enumerating the strings of regular
languages . . . . . . . . . . . . . . . 503--518
Mário Florido and
Luís Damas Linearization of the lambda-calculus and
its relation with intersection type
systems . . . . . . . . . . . . . . . . 519--546
Tim Sheard and
Emir Pasalic Two-level types and parameterized
modules . . . . . . . . . . . . . . . . 547--587
Nimish Shah Book Review: \booktitleKnowledge
Representation, Reasoning and
Declarative Problem Solving, by C.
Baral, Cambridge University Press, 2003 588--589
Mike Thomas Book Review: \booktitleReasoning About
Program Transformations: Imperative
Programming and Flow of Data, by
Jean-François Collard, Springer-Verlag,
2003, ISBN 0-387-95391-4 . . . . . . . . 589--592
Fr\`ed\`eric Loulergue Book Review: \booktitleDéveloppement
d'applications avec Objective CAML, by
E. Chailloux, P. Manoury and B. Pagano,
O'Reilley, 2003 . . . . . . . . . . . . 592--594
Peter Hancock Book Review: \booktitleThe Fun of
Programming, edited by Jeremy Gibbons
and Oege de Moor, Palgrave Macmillan,
2003, ISBN 1-4039-0772-2 (HB),
0-333-99285-7 (SB) . . . . . . . . . . . 594--597
John Derrick Book Review: \booktitleProgramming
Methodology. A. McIver and C. Morgan,
editors, Springer-Verlag, 2002, ISBN
0-387-95349-3 . . . . . . . . . . . . . 597--598
Nimish Shah Book Review: \booktitleProgram
Construction: Calculating
Implementations from Specifications, by
R. C. Backhouse, John Wiley & Sons, 2004 598--600
Ralf Hinze Special issue on functional pearls:
Editorial . . . . . . . . . . . . . . . 601--601
Richard S. Bird and
Shin-Cheng Mu Functional Pearl: Inverting the
Burrows--Wheeler transform . . . . . . . 603--612
Richard S. Bird Functional Pearl: On tiling a chessboard 613--622
Harry G. Mairson Functional Pearl: Linear lambda calculus
and PTIME-completeness . . . . . . . . . 623--633
Arthur I. Baars and
Andres Löh and
S. Doaitse Swierstra Functional Pearl: Parsing permutation
phrases . . . . . . . . . . . . . . . . 635--646
Luc Maranget Functional Pearl: Functional
satisfaction . . . . . . . . . . . . . . 647--656
Sergio Antoy and
Michael Hanus Functional Pearl: Concurrent distinct
choices . . . . . . . . . . . . . . . . 657--668
Peter Ljunglöf Functional Pearl: Functional chart
parsing of context-free grammars . . . . 669--680
Stephanie Weirich Functional Pearl: Type-safe cast . . . . 681--695
John T. O'Donnell and
Gudula Rünger Functional Pearl: Derivation of a
logarithmic time carry lookahead
addition circuit . . . . . . . . . . . . 697--713
Mark P. Jones Functional Pearl: Composing fractals . . 715--725
Andrew J. Kennedy Functional Pearl: Pickler combinators 727--739
Koen Claessen Functional Pearl: Parallel Parsing
Processes . . . . . . . . . . . . . . . 741--757
Lambert Meertens Functional Pearl: Calculating the Sieve
of Eratosthenes . . . . . . . . . . . . 759--763
Ralf Hinze Theoretical Pearl: Church numerals,
twice! . . . . . . . . . . . . . . . . . 1--13
Lloyd Allison Models for machine learning and data
mining in functional programming . . . . 15--32
R. David and
G. Mounier An intuitionistic $ \lambda $-calculus
with exceptions . . . . . . . . . . . . 33--52
Kurt Nòrmark Web programming in Scheme with LAML . . 53--65
Ricardo Peña and
Clara Segura Non-determinism analyses in a
parallel-functional language . . . . . . 67--100
Vasco Thudichum Vasconcelos Lambda and pi calculi, CAM and SECD
machines . . . . . . . . . . . . . . . . 101--127
Martín Abadi and
Greg Morrisett and
Andrei Sabelfeld ``Language-Based Security'' . . . . . . 129--129
Anindya Banerjee and
David A. Naumann Stack-based access control and secure
information flow . . . . . . . . . . . . 131--177
Frédéric Besson and
Thomas De Grenier De Latour and
Thomas Jensen Interfaces for stack inspection . . . . 179--217
Eduardo Bonelli and
Adriana Compagnoni and
Elsa Gunter Correspondence assertions for process
synchronization in concurrent
communications . . . . . . . . . . . . . 219--247
Karl Crary and
Aleksey Kliger and
Frank Pfenning A monadic analysis of information flow
security with mutable state . . . . . . 249--291
Kohei Honda and
Nobuko Yoshida Noninterference through flow analysis 293--349
P. W. Trinder Special Issue High Performance Parallel
Functional Programming . . . . . . . . . 351--352
Clemens Grelck Shared memory multiprocessor support for
functional array processing in SAC . . . 353--401
Victor M. Gulias and
Miguel Barreiro and
Jose L. Freire VoDKA: Developing a Video-on-Demand
Server using Distributed Functional
Programming . . . . . . . . . . . . . . 403--430
Rita Loogen and
Yolanda Ortega-Mallén and
Ricardo Peña-Marí Parallel functional programming in Eden 431--475
Edward A. Luke and
Thomas George Loci: a rule-based framework for
parallel multi-disciplinary simulation
synthesis . . . . . . . . . . . . . . . 477--502
Nick Benton Embedded interpreters . . . . . . . . . 503--542
Cristiano Calcagno and
Luca Cardelli and
Andrew D. Gordon Deciding validity in a spatial logic for
trees . . . . . . . . . . . . . . . . . 543--572
Gérard Huet A functional toolkit for morphological
and phonological processing, application
to a Sanskrit tagger . . . . . . . . . . 573--614
Norman Scaife and
Susumi Horiguchi and
Greg Michaelson and
Paul Bristow A parallel SML compiler based on
algorithmic skeletons . . . . . . . . . 615--650
Stefan Kahrs Book Review: \booktitleTerm Rewriting
Systems, by ``Terese'', Cambridge
University Press, 2003 . . . . . . . . . 651--651
Dipanwita Sarkar and
Oscar Waddell and
R. Kent Dybvig Educational Pearl: A Nanopass framework
for compiler education . . . . . . . . . 653--667
Peter Mòller Neergaard Theoretical Pearls: A bargain for
intersection types: a simple strong
normalization proof . . . . . . . . . . 669--677
Richard Bird and
Shin-Cheng Mu Countdown: A case study in origami
programming . . . . . . . . . . . . . . 679--702
Alessandra Di Pierro and
Chris Hankin and
Herbert Wiklicky Quantitative static analysis of
distributed systems . . . . . . . . . . 703--749
Erick Gallesio and
Manuel Serrano Skribe: a functional authoring language 751--770
Fairouz Kamareddine Typed $ \lambda $-calculi with one
binder . . . . . . . . . . . . . . . . . 771--796
Chiyan Chen and
Hongwei Xi Meta-programming through typeful code
representation . . . . . . . . . . . . . 797--835
William L. Harrison and
Richard B. Kieburtz The logic of demand in Haskell . . . . . 837--891
Aleksandar Nanevski and
Frank Pfenning Staged computation with names and
necessity . . . . . . . . . . . . . . . 893--939
David Wakeling Educational Pearl: Biological sequence
similarity . . . . . . . . . . . . . . . 1--12
Richard Bird and
Sharon Curtis Functional Pearls: Finding celebrities:
A lesson in functional programming . . . 13--20
Martin Erwig and
Steve Kollmansberger Functional Pearls: Probabilistic
functional programming in Haskell . . . 21--34
Per Gustafsson and
Konstantinos Sagonas Efficient manipulation of binary data
using pattern matching . . . . . . . . . 35--74
Ketil Malde and
Robert Giegerich Calculating PSSM probabilities with lazy
dynamic programming . . . . . . . . . . 75--81
Tian Zhao and
Jens Palsberg and
Jan Vitek Type-based confinement . . . . . . . . . 83--128
S. A. Curtis Functional Pearl: Marble mingling . . . 129--136
Gilles Barthe and
Thierry Coquand Remarks on the equational theory of
non-normalizing pure type systems . . . 137--155
Jim Grundy and
Tom Melham and
John O'Leary A reflective functional language for
hardware design and theorem proving . . 157--196
Ralf Hinze and
Ross Paterson Finger trees: a simple general-purpose
data structure . . . . . . . . . . . . . 197--217
Robin Adams Pure type systems with judgemental
equality . . . . . . . . . . . . . . . . 219--246
Nimish Shah Book Review: \booktitleAdvanced Topics
in Term Rewriting, by Enno Ohlebusch,
Springer Verlag, 2002 . . . . . . . . . 247--249
David Sankel Book Review: \booktitleThe Haskell Road
to Logic, Maths and Programming, by Kees
Doets and Jan van Eijck, King's College
Publications, 2004, ISBN 0-9543006-9-6 249--250
Isaac Jones Book Review: \booktitleThe Standard ML
Basis Library, by Emden R. Gansner and
John H. Reppy, editors, Cambridge
University Press, 2004, 406 pp. . . . . 250--251
Shriram Krishnamurthi Educational Pearl: Automata via macros 253--267
Dariusz Biernacki and
Olivier Danvy Theoretical Pearl: A simple proof of a
folklore theorem about delimited control 269--280
Jeremy Gibbons and
David Lester and
Richard Bird Functional Pearl: Enumerating the
rationals . . . . . . . . . . . . . . . 281--291
Martin Erwig and
Robin Abraham and
Steve Kollmansberger and
Irene Cooperstein Gencel: a program generator for correct
spreadsheets . . . . . . . . . . . . . . 293--325
Anna Bucalo and
Furio Honsell and
Marino Miculan and
Ivan Scagnetto and
Martin Hoffman Consistency of the theory of contexts 327--372
Kathleen Fisher Introduction . . . . . . . . . . . . . . 373--374
Matthias Blume and
David McAllester Sound and complete models of contracts 375--414
Simon Marlow and
Simon Peyton Jones Making a fast curry: push/enter vs.
eval/apply for higher-order languages 415--449
Ralf Hinze Generics for the masses . . . . . . . . 451--483
Matthew Fluet and
Greg Morrisett Monadic regions . . . . . . . . . . . . 485--545
Olin Shivers and
David Fisher Multi-return function call . . . . . . . 547--582
Robert Bruce Findler and
Matthew Flatt Slideshow: functional presentations . . 583--619
Dario Colazzo and
Giorgio Ghelli and
Paolo Manghi and
Carlo Sartiani Static analysis for path correctness of
XML queries . . . . . . . . . . . . . . 621--661
Kwangkeun Yi Educational Pearl: `Proof-directed
debugging' revisited for a first-order
version . . . . . . . . . . . . . . . . 663--670
Richard Bird Functional Pearl: A program to solve
Sudoku . . . . . . . . . . . . . . . . . 671--679
Stephanie Weirich Type-safe run-time polytypic programming 681--710
Haruo Hosaya Regular expression filters for XML . . . 711--750
Matthew Fluet and
Riccardo Pucella Phantom types and subtyping . . . . . . 751--791
Alex Potanin and
James Noble and
Dave Clarke and
Robert Biddle Featherweight generic confinement . . . 793--811
Simon Peyton Jones and
Dimitrios Vytiniotis and
Stephanie Weirich and
Mark Shields Practical type inference for
arbitrary-rank types . . . . . . . . . . 1--82
Martin Sulzmann and
Gregory J. Duck and
Simon Peyton-Jones and
Peter J. Stuckey Understanding functional dependencies
via constraint handling rules . . . . . 83--129
David Wakeling Spreadsheet functional programming . . . 131--143
Ronald Garcia and
Jaakko Jarvi and
Andrew Lumsdaine and
Jeremy Siek and
Jeremiah Willcock An extended comparative study of
language support for generic programming 145--205
Philippe Narbel Type sharing constraints and
undecidability . . . . . . . . . . . . . 207--214
Hongwei Xi Dependent ML An approach to practical
programming with dependent types . . . . 215--286
Judicaël Courant A module calculus for Pure Type Systems 287--352
Gábor M. Surányi An object-oriented calculus with term
constraints . . . . . . . . . . . . . . 353--386
Luc Maranget Warnings for pattern matching . . . . . 387--421
Peter King Book Review: \booktitleSMIL 2.0
Interactive Multimedia for Web and
Mobile Devices, by Dick C. A. Bulterman
and Lloyd Rutledge, Springer
X.media.publishing, 2004, 440 pp., ISBN
3-540-20234-X . . . . . . . . . . . . . 423--424
Alex Simpson Book Review: \booktitleProgramming
Languages and Operational Semantics, by
Maribel Fernández, King's College
Publications, 2004, ISBN 0-9543006-3-7 424--426
Isaac Jones Book Review: \booktitleThe Haskell
School of Expression, by Paul Hudak,
Cambridge Univerity Press, 2000 1 . . . 426--428
Greg Michaelson Book Review: \booktitleInductive
Synthesis of Functional Programs, by
Schmid U., Springer-Verlag, 2003, 420
pp., ISBN 3-540-40174-1 . . . . . . . . 428--429
Matthew Flatt and
Benjamin C. Pierce Preface . . . . . . . . . . . . . . . . 431--431
Derek Dreyer Recursive type generativity . . . . . . 433--471
Martin Berger and
Kohei Honda and
Nobuko Yoshida A logical analysis of aliasing in
imperative higher-order functions . . . 473--546
Peter Sewell and
James J. Leifer and
Keith Wansbrough and
Francesco Zappa Nardelli and
Mair Allen-Williams and
Pierre Habouzit and
Viktor Vafeiadis Acute: High-level programming language
design for distributed computation . . . 547--612
Robert Harper and
Daniel R. Licata Mechanizing metatheory in a logical
framework . . . . . . . . . . . . . . . 613--673
Rex Page Engineering Software Correctness . . . . 675--686
R. Kent Dyvbig and
Simon Peyton Jones and
Amr Sabry A monadic framework for delimited
continuations . . . . . . . . . . . . . 687--730
Neil Ghani and
Patricia Johann Monadic augment and generalised short
cut fusion . . . . . . . . . . . . . . . 731--776
Graham Hutton and
Joel Wright What is the meaning of these constant
interruptions? . . . . . . . . . . . . . 777--792
Olivier Danvy and
Kevin Millikin and
Lasse R. Nielsen On one-pass CPS transformations . . . . 793--812
Alicia Villanueva Book Review: \booktitleVerification of
Reactive Systems, by Schneider, Klaus,
Springer-Verlag, 2003, 600 pp., ISBN
3-540-00296-0 . . . . . . . . . . . . . 813--814
Conor Mcbride and
Ross Paterson Applicative programming with effects . . 1--13
David A. Greve and
Matt Kaufmann and
Panagiotis Manolios and
J. Strother Moore and
Sandip Ray and
José Luis Ruiz-Reina and
Rob Sumners and
Daron Vroon and
Matthew Wilding Efficient execution in an automated
reasoning environment . . . . . . . . . 15--46
Jacob Matthews and
Robert Bruce Findler An operational semantics for Scheme 1 47--86
Geoffrey Washburn and
Stephanie Weirich Boxes go bananas: Encoding higher-order
abstract syntax with parametric
polymorphism . . . . . . . . . . . . . . 87--140
David Aspinall and
Martin Hofmann and
Michal Konecný A type system with usage aspects . . . . 141--178
Christian Skalka and
Scott Smith and
David Van Horn Types and trace effects of higher order
programs . . . . . . . . . . . . . . . . 179--249
Martin Sulzmann and
Peter J. Stuckey HM(X) type inference is CLP(X) solving 251--283
Chieri Saito and
Atsushi Igarashi and
Mirko Viroli Lightweight family polymorphism . . . . 285--331
Koichi Kodama and
Kohei Suenaga and
Naoki Kobayashi Translation of tree-processing programs
into stream-processing programs based on
ordered linear type . . . . . . . . . . 333--371
Zena M. Ariola and
Hugo Herbelin Control reduction theories: the benefit
of structural substitution . . . . . . . 373--419
Gergely Buday Book Review: \booktitleLogic in Computer
Science: Modelling and Reasoning About
Systems, by Huth Michael and Ryan Mark,
second edition. ISBN 0-521-54310-X . . . 421--422
Wouter Swierstra Data types \`a la carte . . . . . . . . 423--436
Peter Sewell and
Gareth Stoyle and
Michael Hicks and
Gavin Bierman and
Keith Wansbrough Dynamic rebinding for marshalling and
update, via redex-time and destruct-time
reduction . . . . . . . . . . . . . . . 437--502
Manfred Schmidt-Schauss and
David Sabel and
Marko Schütz Safety of Nöcker's strictness analysis 503--551
Yaron Minsky and
Stephen Weeks Caml trading --- experiences with
functional programming on Wall Street 553--564
Julia Lawall Editorial . . . . . . . . . . . . . . . 565--566
Björn Bringert and
Aarne Ranta A pattern for almost compositional
functions . . . . . . . . . . . . . . . 567--598
Adam Chlipala Modular development of certified program
verifiers with a proof assistant 1, 2 599--647
Kevin Donnelly and
Matthew Fluet Transactional events . . . . . . . . . . 649--706
David Fisher and
Olin Shivers Building language towers with Ziggurat 707--780
Shin-Ya Katsumata and
Susumu Nishimura Algebraic fusion of functions with an
accumulating parameter and its
improvement . . . . . . . . . . . . . . 781--819
Matthew Might and
Olin Shivers Exploiting reachability and cardinality
in higher-order flow analysis . . . . . 821--864
Aleksandar Nanevski and
Greg Morrisett and
Lars Birkedal Hoare type theory, polymorphism and
separation . . . . . . . . . . . . . . . 865--911
S. Doaitse Swierstra and
Olaf Chitil Linear, bounded, functional
pretty-printing . . . . . . . . . . . . 1--16
Hayo Thielecke Control effects as a modality . . . . . 17--26
Simon Frankau and
Diomidis Spinellis and
Nick Nassuphis and
Christoph Burgard Commercial uses: Going functional on
exotic trades . . . . . . . . . . . . . 27--45
Alberto De La Encina and
Ricardo Peña From natural semantics to C: A formal
derivation of two STG machines . . . . . 47--94
Melissa E. O'Neill The Genuine Sieve of Eratosthenes . . . 95--106
Sungwoo Park and
Hyeonseung Im Type-safe higher-order channels with
channel locality . . . . . . . . . . . . 107--142
Xavier Leroy Editorial . . . . . . . . . . . . . . . 143--143
Morten Rhiger Type-safe pattern combinators . . . . . 145--156
Jan Schwinghammer Coherence of subsumption for monadic
types . . . . . . . . . . . . . . . . . 157--172
Scott Owens and
John Reppy and
Aaron Turon Regular-expression derivatives
re-examined . . . . . . . . . . . . . . 173--190
Barry Jay and
Delia Kesner First-class patterns . . . . . . . . . . 191--225
Andy Gill and
Graham Hutton The worker/wrapper transformation . . . 227--251
Anthony M. Sloane Book Review: \booktitleSoftware
Abstractions: Logic, Language, and
Analysis, by Jackson Daniel, The MIT
Press, 2006, 366 pp., ISBN
978-0-262-10114-1 . . . . . . . . . . . 253--254
Peter Gammie Book Review: Roy Peter Van and Haridi
Seif. \booktitleConcepts, Techniques,
and Models of Computer Programming. The
MIT Press, 2004. ISBN: 0-262-22069-5
Price \$70. 930 pp.} . . . . . . . . . . 254--256
Saketh Bhamidipati Book Review: \booktitleProgramming in
Haskell, by Hutton Graham, Cambridge
University Press, 2007, 184 pp., ISBN
0-521-69269-5 . . . . . . . . . . . . . 256--259
Krishna Sankar Book Review: \booktitleProgramming
Erlang --- Software for a Concurrent
World, by Armstrong Joe, Pragmatic
Bookshelf, 2007, pp. 536. ISBN-10:
1-934356-00-X . . . . . . . . . . . . . 259--261
Robert Harper Functional Pearl: Proof-directed
debugging --- Corrigendum . . . . . . . 262--262
Anonymous JFP volume 19 issue 2 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 19 issue 2 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
Conor McBride and
Tarmo Uustalu Preface . . . . . . . . . . . . . . . . 263--264
Stephen Lack and
John Power Gabriel-Ulmer duality and Lawvere
theories enriched over a general base 265--286
Andreas Abel Implementing a normalizer using sized
heterogeneous types . . . . . . . . . . 287--310
Thorsten Altenkirch and
James Chapman Big-step normalisation . . . . . . . . . 311--333
Robert Atkey Parameterised notions of computation . . 335--376
Jeremy Gibbons and
Bruno C. d. S. Oliveira The essence of the Iterator pattern . . 377--402
Bart Jacobs and
Chris Heunen and
Ichiro Hasuo Categorical semantics for arrows . . . . 403--438
Ralph Matthes An induction principle for nested
datatypes in intensional type theory . . 439--468
J. Michael Spivey Algebras for combinatorial search . . . 469--487
Anonymous JFP volume 19 issue 3-4 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 19 issue 3-4 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b8
Xavier Leroy and
Matthias Felleisen Editorial . . . . . . . . . . . . . . . 489--490
Ralf Hinze The Bird Tree . . . . . . . . . . . . . 491--508
Jacques Carette and
Oleg Kiselyov and
Chung-Chieh Shan Finally tagless, partially evaluated:
Tagless staged interpreters for simpler
typed languages . . . . . . . . . . . . 509--543
Shin-Cheng Mu and
Hsiang-Shang Ko and
Patrik Jansson Algebra of programming in Agda:
Dependent types for relational program
derivation . . . . . . . . . . . . . . . 545--579
Ariel Arbiser and
Alexandre Miquel and
Alejandro Ríos The $ \lambda $-calculus with
constructors: Syntax, confluence and
separation . . . . . . . . . . . . . . . 581--631
Anonymous JFP volume 19 issue 5 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 19 issue 5 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b3
Ralf Hinze Purely Functional 1--2 Brother Trees . . 633--644
Eric Walkingshaw and
Martin Erwig A domain-specific language for
experimental game theory . . . . . . . . 645--661
Tom Schrijvers and
Peter Stuckey and
Philip Wadler Monadic constraint programming . . . . . 663--697
Keiko Nakata and
Masahito Hasegawa Small-step and big-step semantics for
call-by-need . . . . . . . . . . . . . . 699--722
Olaf Chitil Book Review: \booktitleEssentials of
Programming Languages (third edition),
by Friedman Daniel P. and Wand Mitchell,
MIT Press, ISBN 978-0-262-06279-4, 2008 723--725
Anonymous JFP volume 19 issue 6 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 19 issue 6 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b5
Michael Sperber and
R. Kent Dybvig and
Matthew Flatt and
Anton Van Straaten and
Robby Findler and
Jacob Matthews Revised 6 Report on the Algorithmic
Language Scheme . . . . . . . . . . . . 1--301
Anonymous JFP volume 19 issue S1 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 19 issue S1 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
Jeremy Gibbons Editorial . . . . . . . . . . . . . . . 1--1
John Clements and
Kathi Fisler ``Little language'' project modules . . 3--18
Simon J. Gay and
Vasco T. Vasconcelos Linear type theory for asynchronous
session types . . . . . . . . . . . . . 19--50
Sam Lindley and
Philip Wadler and
Jeremy Yallop The arrow calculus . . . . . . . . . . . 51--69
Peter Sewell and
Francesco Zappa Nardelli and
Scott Owens and
Gilles Peskine and
Thomas Ridge and
Susmit Sarkar and
Rok Strnisa Ott: Effective tool support for the
working semanticist . . . . . . . . . . 71--122
Anonymous JFP volume 20 issue 1 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 20 issue 1 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b8
Jeremy Wazny Experience report: Functional
programming in C-Rules . . . . . . . . . 123--136
Lukasz Ziarek and
Suresh Jagannathan Lightweight checkpointing for concurrent
ML . . . . . . . . . . . . . . . . . . . 137--173
Dimitrios Vytiniotis and
Stephanie Weirich Parametricity, type equality, and
higher-order polymorphism . . . . . . . 175--210
Anonymous JFP volume 20 issue 2 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 20 issue 2 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b10
Ralf Hinze Special Issue on Generic Programming
Editorial . . . . . . . . . . . . . . . 211--212
Wendy Verbruggen and
Edsko De Vries and
Arthur Hughes Formal polytypic programs and proofs . . 213--270
Jean-Philippe Bernardy and
Patrik Jansson and
Marcin Zalewski and
Sibylle Schupp Generic programming with C++ concepts
and Haskell type classes --- a
comparison . . . . . . . . . . . . . . . 271--302
Bruno C. D. S. Oliveira and
Jeremy Gibbons Scala for generic programmers: Comparing
Haskell and Scala support for generic
programming . . . . . . . . . . . . . . 303--352
Graham Hutton and
Mauro Jaskelioff and
Andy Gill Factorising folds for faster functions 353--373
Thomas Van Noort and
Alexey Rodriguez Yakushev and
Stefan Holdermans and
Johan Jeuring and
Bastiaan Heeren and
José Pedro Magalhães A lightweight approach to
datatype-generic rewriting . . . . . . . 375--413
Anonymous JFP volume 20 issue 3-4 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 20 issue 3-4 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b7
Peter Thiemann and
Henrik Nilsson Special Issue Dedicated to ICFP 2008
Editorial . . . . . . . . . . . . . . . 415--416
Daniel Spoonhower and
Guy E. Blelloch and
Robert Harper and
Phillip B. Gibbons Space profiling for parallel functional
programs . . . . . . . . . . . . . . . . 417--461
Ralf Hinze Concrete stream calculus: An extended
study . . . . . . . . . . . . . . . . . 463--535
Matthew Fluet and
Mike Rainey and
John Reppy and
Adam Shaw Implicitly threaded parallelism in
Manticore . . . . . . . . . . . . . . . 537--576
Eelco Dolstra and
Andres Löh and
Nicolas Pierron NixOS: A purely functional Linux
distribution . . . . . . . . . . . . . . 577--615
Anonymous JFP volume 20 issue 5-6 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 20 issue 5-6 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b8
Peter Achten The Soccer-Fun project . . . . . . . . . 1--19
Sungwoo Park and
Hyeonseung Im A calculus for hardware description . . 21--58
Mary Sheeran Functional and dynamic programming in
the design of parallel prefix networks 59--114
Peter Gammie Book Review: \booktitleLambda-Calculus
and Combinators: An Introduction, Second
Edition, by Hindley, J. R. and Seldin,
J. P. . . . . . . . . . . . . . . . . . 115--117
Anonymous JFP volume 21 issue 1 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 21 issue 1 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b5
Richard S. Bird Building a consensus: A rectangle
covering problem . . . . . . . . . . . . 119--128
Maarten Fokkinga The Hough transform . . . . . . . . . . 129--133
Oliver Friedmann and
Martin Lange More on balanced diets . . . . . . . . . 135--157
Johannes Borgström and
Andrew D. Gordon and
Riccardo Pucella Roles, stacks, histories: A triple for
Hoare . . . . . . . . . . . . . . . . . 159--207
Peter Gammie Short note: Strict unwraps make
workerg/wrapper fusion totally correct 209--213
Jurriaan Hage Book Review: \booktitleLanguage
Implementation Patterns: Create your own
Domain-Specific and General Programming
Languages, by Parr Terence, Pragmatic
Bookshelf, http://www.pragprog.com, ISBN
978-1-934356-45-6 . . . . . . . . . . . 215--217
Willem De Jong Book Review: \booktitleFoundations of
F#, Pickering Robert, Apress, 2007 ISBN
10: 1-59059-757-5 . . . . . . . . . . . 217--218
Anonymous JFP volume 21 issue 2 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 21 issue 2 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b6
Ralf Hinze Typed quote/antiquote or: Compile-time
parsing . . . . . . . . . . . . . . . . 219--234
Andrew M. Pitts Structural recursion with locally scoped
names . . . . . . . . . . . . . . . . . 235--286
Yoichi Hirai and
Kazuhiko Yamamoto Balancing weight-balanced trees . . . . 287--307
Barney Stratford A combinator library for the design of
railway track layouts . . . . . . . . . 309--329
Anonymous JFP volume 21 issue 3 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 21 issue 3 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b3
Andrew Tolmach and
Xavier Leroy Special Issue Dedicated to ICFP 2009
Editorial . . . . . . . . . . . . . . . 331--332
Dimitrios Vytiniotis and
Simon Peyton Jones and
Tom Schrijvers and
Martin Sulzmann OutsideIn(X) Modular type inference with
local assumptions . . . . . . . . . . . 333--412
Sebastian Fischer and
Oleg Kiselyov and
Chung-Chieh Shan Purely functional lazy nondeterministic
programming . . . . . . . . . . . . . . 413--465
Hai Liu and
Eric Cheng and
Paul Hudak Causal commutative arrows . . . . . . . 467--496
Georg Neis and
Derek Dreyer and
Andreas Rossberg Non-parametric parametricity . . . . . . 497--562
Anonymous JFP volume 21 issue 4--5 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 21 issue 4--5 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
Matti Nykänen A note on the genuine Sieve of
Eratosthenes . . . . . . . . . . . . . . 563--572
Wouter Swierstra Sorted: Verifying the Problem of the
Dutch National Flag in Agda . . . . . . 573--583
Norman Ramsey Embedding an interpreted language using
higher-order functions and types . . . . 585--615
Yukiyoshi Kameyama and
Oleg Kiselyov and
Chung-Chieh Shan Shifting the stage: Staging with
delimited control . . . . . . . . . . . 617--662
Jacques Carette Book Review: \booktitleHandbook of
Practical Logic and Automated Reasoning,
by Harrison John, Cambridge University
Press, 2009 ISBN 978-0-521-89957-4 . . . 663--664
Toni Cebrián Book Review: \booktitleHow to think
about algorithms, by Edmonds Jeff,
Cambridge University Press, ISBN
0-521-61410-4 . . . . . . . . . . . . . 664--666
Anonymous JFP volume 21 issue 6 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 21 issue 6 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
Anil Madhavapeddy and
Yaron Minsky and
Marius Eriksen CUFP 2011 Workshop Report . . . . . . . 1--8
Klaus Aehlig and
Florian Haftmann and
Tobias Nipkow A compiled implementation of
normalisation by evaluation . . . . . . 9--30
Gavin M. Bierman and
Andrew D. Gordon and
Catalin Hritcu and
David Langworthy Semantic subtyping with an SMT solver 31--105
Anonymous JFP volume 22 issue 1 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 22 issue 1 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b9
Jean-Philippe Bernardy and
Patrik Jansson and
Ross Paterson Proofs for free: Parametricity for
dependent types . . . . . . . . . . . . 107--152
Vincent Siles and
Hugo Herbelin Pure Type System conversion is always
typable . . . . . . . . . . . . . . . . 153--180
Matthew Flatt and
Ryan Culpepper and
David Darais and
Robert Bruce Findler Macros that Work Together: Compile-time
bindings, partial expansion, and
definition contexts . . . . . . . . . . 181--216
Eerke Boiten Book Review: \booktitleModeling in
Event-B --- System and Software
Engineering, Abrial Jean-Raymond,
Cambridge University Press, May 2010
ISBN-10: 0-521-89556-1 . . . . . . . . . 217--219
Dusan Kol\`ar Book Review: \booktitleDrawing Programs:
The Theory and Practice of Schematic
Functional Programming, by Addis, Tom
and Addis, Jan, Springer, 2010, ISBN
978-1-84882-617-5, 379 pp. . . . . . . . 219--221
Anonymous JFP volume 22 issue 2 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 22 issue 2 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b7
Matthias Felleisen Editorial . . . . . . . . . . . . . . . 223--224
Michael Greenberg and
Benjamin C. Pierce and
Stephanie Weirich Contracts made manifest . . . . . . . . 225--274
Akimasa Morihata and
Kazuhiko Kakehi and
Zhenjiang Hu and
Masato Takeichi Manipulating accumulative functions by
swapping call-time and return-time
computations . . . . . . . . . . . . . . 275--299
Fritz Henglein Generic top-down discrimination for
sorting and partitioning in linear time 300--374
Jurriaan Hage Book Review: \booktitleBookreview JFP:
Domain-Specific Languages, by Martin
Fowler The Addison Wesley Signature
Series . . . . . . . . . . . . . . . . . 375--377
Anonymous JFP volume 22 issue 3 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 22 issue 3 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b7
Umut A. Acar and
James Cheney and
Stephanie Weirich Editorial: Special issue dedicated to
ICFP 2010 . . . . . . . . . . . . . . . 379--381
Lars Bergstrom and
Matthew Fluet and
Mike Rainey and
John Reppy and
Adam Shaw Lazy tree splitting . . . . . . . . . . 382--438
Ryan Culpepper Fortifying macros . . . . . . . . . . . 439--476
Derek Dreyer and
Georg Neis and
Lars Birkedal The impact of higher-order state and
control effects on local relational
reasoning . . . . . . . . . . . . . . . 477--528
Andrew J. Kennedy and
Dimitrios Vytiniotis Every bit counts: The binary
representation of typed data and
programs . . . . . . . . . . . . . . . . 529--573
Matthew Naylor and
Colin Runciman The Reduceron reconfigured and
re-evaluated . . . . . . . . . . . . . . 574--613
Nicolas Pouillard and
François Pottier A unified treatment of syntax with
binders . . . . . . . . . . . . . . . . 614--704
David Van Horn and
Matthew Might Systematic abstraction of abstract
machines . . . . . . . . . . . . . . . . 705--746
Anonymous JFP volume 22 issue 4--5 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 22 issue 4--5 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
Michael Spivey When Maybe is not good enough . . . . . 747--756
Dominique Devriese and
Frank Piessens Finally tagless observable recursion for
an abstract grammar model . . . . . . . 757--796
Bruno C. D. S. Oliveira and
Tom Schrijvers and
William R. Cook MRI: Modular reasoning about
interference in incremental programming 797--852
Neil Brown Book Review: \booktitleFunctional
Programming for Java Developers ---
Tools for Better Concurrency,
Abstraction, and Agility, By Dean
Wampler, O'Reilly Media, July 2011,
ISBN-13: 978-1-4493-1103-2, 90 pp. . . . 853--854
Toni Cebrián Book Review: \booktitleSteps in Scala:
An introduction to Object-Functional
Programming, by Christos K. K. Loverdos,
Apostolos Syropoulos, Cambridge
University Press, 2010, 504 pp., ISBN
0-521-74758-9 . . . . . . . . . . . . . 854--855
Anonymous JFP volume 22 issue 6 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 22 issue 6 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b5
Brigitte Pientka An insider's look at LF type
reconstruction: everything you (n)ever
wanted to know . . . . . . . . . . . . . 1--37
François Pottier Syntactic soundness proof of a
type-and-capability system with hidden
state . . . . . . . . . . . . . . . . . 38--144
Anonymous JFP volume 23 issue 1 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 23 issue 1 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
Mark P. Jones Solving the snake cube puzzle in Haskell 145--160
Keisuke Nakano Metamorphism in jigsaw . . . . . . . . . 161--173
Richard S. Bird An in-situ algorithm for expanding a
graph . . . . . . . . . . . . . . . . . 174--184
Peter Achten and
Marko Van Eekelen and
Maarten De Mol and
Rinus Plasmeijer EditorArrow: An arrow-based model for
editor-based programming . . . . . . . . 185--224
Laura Castro Book Review: \booktitleBuilding Web
Applications with Erlang, by Zachary
Kessin, O'Reilly Media, Inc., 2012, ISBN
97-81-4493-20652 . . . . . . . . . . . . 225--226
Ivan Lazar Miljenovic Book Review: \booktitlePearls of
Functional Algorithm Design, by Richard
Bird, Cambridge University Press,
September 2010, \pounds 35.00, US
\$60.00. ISBN: 978-0-521-51338-8
(hardback), 286 pp.} . . . . . . . . . . 226--227
Anonymous JFP volume 23 issue 2 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 23 issue 2 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b3
Wouter Swierstra and
Thomas Van Noort A library for polymorphic dynamic typing 229--248
Umut A. Acar and
Matthias Blume and
Jacob Donham A consistent semantics of self-adjusting
computation . . . . . . . . . . . . . . 249--292
Simon Thompson and
Huiqing Li Refactoring tools for functional
languages . . . . . . . . . . . . . . . 293--350
Greg Michaelson Book Review: \booktitleLearn You a
Haskell for Great Good! A Beginner's
Guide, by Miran Lipovaca, No Starch
Press, April 2011, ISBN-10:
1-59327-283-9; ISBN-13:
978-1-59327-283-8, 376 pp. . . . . . . . 351--352
Prabhakar Ragde Book Review: \booktitleOCaml from the
Very Beginning, by John Whitington,
Coherent Press, 2013, \pounds 25.99, US
\$37.99. ISBN-10: 0-9576711-0-5
(paperback), 204 pp.} . . . . . . . . . 352--354
Anonymous JFP volume 23 issue 3 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 23 issue 3 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b4
Kenichi Asai and
Benjamin C. Pierce Special Issue Dedicated to ICFP 2011
Editorial . . . . . . . . . . . . . . . 355--356
Georges Gonthier and
Beta Ziliani and
Aleksandar Nanevski and
Derek Dreyer How to make ad hoc proof automation less
ad hoc . . . . . . . . . . . . . . . . . 357--401
Nikhil Swamy and
Juan Chen and
Cédric Fournet and
Pierre-Yves Strub and
Karthikeyan Bhargavan and
Jean Yang Secure distributed programming with
value-dependent types . . . . . . . . . 402--451
Alexey Gotsman and
Hongseok Yang Modular verification of preemptive OS
kernels . . . . . . . . . . . . . . . . 452--514
Anonymous JFP volume 23 issue 4 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 23 issue 4 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b2
Janis Voigtländer and
Zhenjiang Hu and
Kazutaka Matsuda and
Meng Wang Enhancing semantic bidirectionalization
via shape bidirectionalizer plug-ins . . 515--551
Edwin Brady Idris, a general-purpose dependently
typed programming language: Design and
implementation . . . . . . . . . . . . . 552--593
Katarzyna Grygiel and
Pierre Lescanne Counting and generating lambda terms . . 594--628
Anonymous JFP volume 23 issue 5 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 23 issue 5 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b8
C. E. Martin and
S. A. Curtis Fractal image compression . . . . . . . 629--657
Matthew R. Lakin and
Andrew M. Pitts Contextual equivalence for inductive
definitions with binders in higher order
typed functional programming . . . . . . 658--700
Michael Sperber and
Anil Madhavapeddy Commercial users of functional
programming workshop report . . . . . . 701--712
Anonymous JFP volume 23 issue 6 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 23 issue 6 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b6
Paul Downen and
Zena M. Ariola Delimited control and computational
effects . . . . . . . . . . . . . . . . 1--55
Yan Chen and
Joshua Dunfield and
Matthew A. Hammer and
Umut A. Acar Implicit self-adjusting computation for
purely functional programs . . . . . . . 56--112
Neil Sculthorpe and
Graham Hutton Work it, wrap it, fix it, fold it . . . 113--127
Michael Sperber Book Review: \booktitleSystematic
Program Design: From Clarity to
Efficiency, by Yanhong Annie Liu,
Cambridge University Press, 2013, ISBN:
978-1-107-03660-4 . . . . . . . . . . . 128--130
Anonymous JFP volume 24 issue 1 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 24 issue 1 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b8
Satnam Singh and
Robert Bruce Findler Special Issue Dedicated to ICFP 2012:
Editorial . . . . . . . . . . . . . . . 131--132
Joshua Dunfield Elaborating intersection and union types 133--165
Jörg Endrullis and
Dimitri Hendriks and
Rena Bakhshi and
Grigore Rosu On the complexity of stream equality . . 166--217
J. Ian Johnson and
Ilya Sergey and
Christopher Earl and
Matthew Might and
David Van Horn Pushdown flow analysis with abstract
garbage collection . . . . . . . . . . . 218--283
Magnus O. Myreen and
Scott Owens Proof-producing translation of
higher-order logic into pure and
stateful ML . . . . . . . . . . . . . . 284--315
Pierre-Évariste Dagand and
Conor McBride Transporting functions across ornaments 316--383
Philip Wadler Propositions as sessions . . . . . . . . 384--418
Matt Jadud Book Review: \booktitleRealm of Racket,
by Forrest Bice, Rose DeMaio, Spencer
Florence, Feng-Yun Mimi Lin, Scott
Lindeman, Nicole Nussbaum, Eric
Peterson, Ryan Plessner, David Van Horn,
Matthias Felleisen and Conrad Barski,
MD, No Starch Press, San Francisco, CA,
2013, \pounds 27.49. ISBN-10:
1-59327-491-2 . . . . . . . . . . . . . 419--421
Robin Green Book Review: \booktitleBeginning
Haskell, by Alejandro Serrano Mena,
Apress, New York City, NY, 2014,
ISBN-10: 1-4302-6250-8, 428 pp. . . . . 421--422
Anonymous JFP volume 24 issue 2--3 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 24 issue 2--3 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b6
Kimball Germane and
Matthew Might Deletion: The curse of the red-black
tree . . . . . . . . . . . . . . . . . . 423--433
Neil Sculthorpe and
Nicolas Frisby and
Andy Gill The Kansas University rewrite engine: A
Haskell-Embedded Strategic Programming
Language with Custom Closed Universes 434--473
Graham Hutton PhD Abstracts . . . . . . . . . . . . . 474--522
David Watt Book Review: \booktitlePractical
Foundations for Programming Languages,
by Robert Harper, Cambridge University
Press, New York, December 2012, English,
ISBN-10: 1-107-02957-0, Hardcover, 487
pp. . . . . . . . . . . . . . . . . . . 523--523
Dominic Orchard Book Review: \booktitleComputational
Semantics with Functional Programming,
by Jan van Eijck and Christina Unger . . 524--527
Anonymous JFP volume 24 issue 4 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 24 issue 4 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b9
Andreas Rossberg and
Claudio Russo and
Derek Dreyer F-ing modules . . . . . . . . . . . . . 529--607
Vlad Patryshev Book Review: \booktitleIntroduction to
the art of programming using Scala, by
Mark C. Lewis, Chapman and Hall/CRC
Press, 2012, \pounds 46.99 (paperback)
ISBN-10: 1-4398-9666-6 . . . . . . . . . 608--609
Anonymous JFP volume 24 issue 5 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 24 issue 5 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b9
Matthias Felleisen Editorial . . . . . . . . . . . . . . . 611--611
Michael Sperber and
Lennart Augustsson Special Issue on Run-Time Systems and
Target Platforms for Functional
Languages: Editorial . . . . . . . . . . 612--612
K. C. Sivaramakrishnan and
Lukasz Ziarek and
Suresh Jagannathan MultiMLton: A multicore-aware runtime
for standard ML . . . . . . . . . . . . 613--674
Andrew W. Keep and
R. Kent Dybvig A run-time representation of Scheme
record types . . . . . . . . . . . . . . 675--716
Anonymous JFP volume 24 issue 6 Cover and Front
matter . . . . . . . . . . . . . . . . . f1--f2
Anonymous JFP volume 24 issue 6 Cover and Back
matter . . . . . . . . . . . . . . . . . b1--b8
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e1
Torsten Grust Book Review: \booktitleThinking
Functionally with Haskell by Richard
Bird, Cambridge University Press, 2014 e2
Marius Eriksen and
Michael Sperber and
Anil Madhavapeddy CUFP'13 scribe's report . . . . . . . . e3
Richard S. Bird How to mingle streams . . . . . . . . . e4
Thorsten Altenkirch and
Neil Ghani and
Peter Hancock and
Conor Mcbride and
Peter Morris Indexed containers . . . . . . . . . . . e5
Hans Georg Schaathun Evaluation of splittable pseudo-random
generators . . . . . . . . . . . . . . . e6
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e7
Koen Claessen and
Jonas Duregård and
Michal H. Palka Generating constrained random data with
uniform distribution . . . . . . . . . . e8
Jesús Aransay and
Jose Divasón Formalisation in higher-order logic and
code generation to functional languages
of the Gauss--Jordan algorithm . . . . . e9
Jean-Philippe Bernardy and
Koen Claessen Efficient parallel and incremental
parsing of practical context-free
languages . . . . . . . . . . . . . . . e10
Ville Tirronen and
Samuel Uusi-mäkelä and
Ville Isomöttönen Understanding beginners' mistakes with
Haskell . . . . . . . . . . . . . . . . e11
Beta Ziliani and
Derek Dreyer and
Neelakantan R. Krishnaswami and
Aleksandar Nanevski and
Viktor Vafeiadis Mtac: A monad for typed tactic
programming in Coq . . . . . . . . . . . e12
Mauro Jaskelioff and
Russell O'Connor A representation theorem for
second-order functionals . . . . . . . . e13
Patrick Bahr and
Graham Hutton Calculating correct compilers . . . . . e14
Amanda Clare Review of ``\booktitleA functional start
to computing with Python'', Ted Herman,
CRC Press, 2014, ISBN 978-1-4665-0455-4 e15
Shane Hudson Review of ``\booktitleLearn you some
Erlang for great good! A beginner's
guide'', by Fred Hébert, No Starch Press,
2013, \pounds 26.80 (paperback), ISBN:
978-1-59327-435-1 . . . . . . . . . . . e16
Jan Hoffmann and
Zhong Shao Type-based amortized resource analysis
with integers and arrays . . . . . . . . e17
Dmitriy Traytel and
Tobias Nipkow Verified decision procedures for MSO on
words based on derivatives of regular
expressions . . . . . . . . . . . . . . e18
Daniel Fridlender and
Miguel Pagano Pure type systems with explicit
substitutions . . . . . . . . . . . . . e19
Robert Atkey and
Patricia Johann Interleaving data and effects . . . . . e20
Graham Hutton PhD abstracts . . . . . . . . . . . . . e21
Sharon Curtis and
Shin-Cheng Mu Calculating a linear-time solution to
the densest-segment problem . . . . . . e22
Ville Tirronen and
Ville Isomöttönen Teaching types with a cognitively
effective worked example format . . . . e23
Katarzyna Grygiel and
Pierre Lescanne Counting and generating terms in the
binary lambda calculus . . . . . . . . . e24
Ralf Hinze and
Nicolas Wu Unifying structured recursion schemes:
An Extended Study . . . . . . . . . . . e1
Andreas Abel and
Brigitte Pientka Well-founded recursion with copatterns
and sized types . . . . . . . . . . . . e2
Aaron Stump and
Peng Fu Efficiency of lambda-encodings in total
type theory . . . . . . . . . . . . . . e3
Catalin Hritcu and
Leonidas Lampropoulos and
Antal Spector-Zabusky and
Arthur Azevedo De Amorim and
Maxime Dén\`es and
John Hughes and
Benjamin C. Pierce and
Dimitrios Vytiniotis Testing noninterference, quickly . . . . e4
Robert Stewart and
Patrick Maier and
Phil Trinder Transparent fault tolerance for scalable
functional computation . . . . . . . . . e5
Bo Joel Svensson and
Ryan R. Newton and
Mary Sheeran A language for hierarchical data
parallel design-space exploration on
GPUs . . . . . . . . . . . . . . . . . . e6
Xavier Clerc OCaml-Java: The Java Virtual Machine as
the target of an OCaml compiler . . . . e7
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e8
K. C. Sivaramakrishnan and
Tim Harris and
Simon Marlow and
Simon Peyton Jones Composable scheduler activations for
Haskell . . . . . . . . . . . . . . . . e9
Jost Berthold and
Hans-Wolfgang Loidl and
Kevin Hammond PAEAN: Portable and scalable runtime
support for parallel Haskell dialects e10
M. Dieterle and
T. Horstmeyer and
R. Loogen and
J. Berthold Skeleton composition versus stable
process systems in Eden . . . . . . . . e11
Pawel Parys A characterization of lambda-terms
transforming numerals . . . . . . . . . e12
Paul Stansifer and
Mitchell Wand Romeo: A system for more flexible
binding-safe programming . . . . . . . . e13
Michael Codish and
Eijiro Sumii Preface for special section from FLOPS
2014 . . . . . . . . . . . . . . . . . . e14
Joachim Breitner and
Richard A. Eisenberg and
Simon Peyton Jones and
Stephanie Weirich Safe zero-cost coercions for Haskell . . e15
Jesper Cockx and
Dominique Devriese and
Frank Piessens Eliminating dependent pattern matching
without K . . . . . . . . . . . . . . . e16
Simon Thompson Review of \booktitleSpreadsheet
implementation technology: Basics and
extensions, by Peter Sestoft, MIT Press,
2014, ISBN 978-0-262-52664-7 . . . . . . e17
Carlo Angiuli and
Edward Morehouse and
Daniel R. Licata and
Robert Harper Homotopical patch theory . . . . . . . . e18
Felipe Bañados Schwerter and
Ronald Garcia and
Éric Tanter Gradual type-and-effect systems . . . . e19
Derek Dreyer and
Mary Sheeran Special issue dedicated to ICFP 2014:
Editorial . . . . . . . . . . . . . . . e20
Noam Zeilberger Linear lambda terms as invariants of
rooted trivalent maps . . . . . . . . . e21
Jun Inoue and
Walid Taha Reasoning about multi-stage programs . . e22
Umut A. Acar and
Arthur Charguéraud and
Mike Rainey Oracle-guided scheduling for controlling
granularity in implicitly parallel
languages . . . . . . . . . . . . . . . e23
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e24
Kuen-Bang Hou (Favonia) and
Nick Benton and
Robert Harper Correctness of compiling polymorphism to
dynamic typing . . . . . . . . . . . . . e1
Hsiang-Shang Ko and
Jeremy Gibbons Programming with ornaments . . . . . . . e2
Phúc C. Nguyên and
Sam Tobin-Hochstadt and
David Van Horn Higher order symbolic execution for
contract verification and refutation . . e3
Luca Padovani A simple library implementation of
binary sessions . . . . . . . . . . . . e4
Deian Stefan and
David Mazi\`eres and
John C. Mitchell and
Alejandro Russo Flexible dynamic information flow
control in the presence of exceptions e5
Maciej Bendkowski Normal-order reduction grammars . . . . e6
Ohad Kammar and
Matija Pretnar No value restriction is needed for
algebraic effects and handlers . . . . . e7
Andreas Abel and
Stephan Adelsberger and
Anton Setzer Interactive programming in Agda ---
Objects and graphical user interfaces e8
Pierre-Evariste Dagand The essence of ornaments . . . . . . . . e9
Beta Ziliani and
Matthieu Sozeau A comprehensible guide to a new unifier
for CIC including universe polymorphism
and overloading . . . . . . . . . . . . e10
Ilya Sergey and
Dimitrios Vytiniotis and
Simon L. Peyton Jones and
Joachim Breitner Modular, higher order cardinality
analysis in theory and practice . . . . e11
Philip Johnson-Freyd and
Paul Downen and
Zena M. Ariola Call-by-name extensionality and
confluence . . . . . . . . . . . . . . . e12
Tarmo Uustalu and
Niccol\`o Veltri Finiteness and rational sequences,
constructively . . . . . . . . . . . . . e13
Aaron Stump The calculus of dependent lambda
eliminations . . . . . . . . . . . . . . e14
Wouter Swierstra and
Peter Dybjer Special issue on Programming with
Dependent Types Editorial . . . . . . . e15
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e16
Maciej Piróg and
Sam Staton Backtracking with cut via a distributive
law and left-zero monoids . . . . . . . e17
Nicholas Smallbone and
Moa Johansson and
Koen Claessen and
Maximilian Algehed Quick specifications for the busy
programmer . . . . . . . . . . . . . . . e18
Max S. New and
Burke Fetscher and
Robert Bruce Findler and
Jay Mccarthy Fair enumeration combinators . . . . . . e19
Graham Hutton and
Patrick Bahr Compiling a 50-year journey . . . . . . e20
Exequiel Rivas and
Mauro Jaskelioff Notions of computation as monoids . . . e21
Jörgen Brandt and
Wolfgang Reisig and
Ulf Leser Computation semantics of the functional
scientific workflow language Cuneiform e22
Nicola Botta and
Patrik Jansson and
Cezar Ionescu Contributions to a computational theory
of policy advice and avoidability . . . e23
Patrick Schultz and
Ryan Wisnesky Algebraic data integration . . . . . . . e24
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e25
João Costa Seco and
Paulo Ferreira and
Hugo Lourenço Capability-based localization of
distributed and heterogeneous queries e26
Leonidas Fegaras An algebra for distributed Big Data
analytics . . . . . . . . . . . . . . . e27
Joachim Breitner The adequacy of Launchbury's natural
semantics for lazy evaluation . . . . . e1
Sheng Chen and
Martin Erwig Systematic identification and
communication of type errors . . . . . . e2
Paul Downen and
Zena M. Ariola A tutorial on computational classical
logic and the sequent calculus . . . . . e3
Cameron Swords and
Amr Sabry and
Sam Tobin-Hochstadt An extended account of contract
monitoring strategies as patterns of
communication . . . . . . . . . . . . . e4
Marco T. Morazán Infusing an HtDP-based CS1 with
distributed programming using functional
video games . . . . . . . . . . . . . . e5
Gabriele Keller and
Fritz Henglein Editorial for the Special Issue on
Parallel and Concurrent Functional
Programming . . . . . . . . . . . . . . e6
Philipp Haller and
Heather Miller and
Normen Müller A programming model and foundation for
lineage-based distributed computation e7
James Cheney and
Torsten Grust Special Issue on Programming Languages
for Big Data Editorial . . . . . . . . . e8
Pierre-Évariste Dagand and
Nicolas Tabareau and
Éric Tanter Foundations of dependent
interoperability . . . . . . . . . . . . e9
Amir Shaikhha and
Mohammad Dashti and
Christoph Koch Push versus pull-based loop fusion in
query engines . . . . . . . . . . . . . e10
Frédéric Blanqui Size-based termination of higher-order
rewriting . . . . . . . . . . . . . . . e11
Jesper Cockx and
Dominique Devriese Proof-relevant unification: Dependent
pattern matching with only the axioms of
your type theory . . . . . . . . . . . . e12
Eric L. Seidel and
Ranjit Jhala and
Westley Weimer Dynamic witnesses for static type errors
(or, Ill-Typed Programs Usually Go
Wrong) . . . . . . . . . . . . . . . . . e13
Ralf Hinze and
Clare Martin Batcher's odd--even merging network
revealed . . . . . . . . . . . . . . . . e14
Kazutaka Matsuda and
Meng Wang Applicative bidirectional programming:
Mixing lenses and semantic
bidirectionalization . . . . . . . . . . e15
Timothy A. K. Zakian and
Trevor L. Mcdonell and
Matteo Cimini and
Ryan R. Newton Ghostbuster: A tool for simplifying and
converting GADTs . . . . . . . . . . . . e16
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e17
Thomas Gilray and
Michael D. Adams and
Matthew Might Abstract allocation as a unified
approach to polyvariance in control-flow
analyses . . . . . . . . . . . . . . . . e18
Ralf Hinze On constructing 2--3 trees . . . . . . . e19
Ralf Jung and
Robbert Krebbers and
Jacques-Henri Jourdan and
Ales Bizjak and
Lars Birkedal and
Derek Dreyer Iris from the ground up: A modular
foundation for higher-order concurrent
separation logic . . . . . . . . . . . . e20
Ralf Hinze and
Clare Martin Parberry's pairwise sorting network
revealed . . . . . . . . . . . . . . . . e21
Andreas Rossberg 1ML --- Core and modules united . . . . e22
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e1
Yong Kiam Tan and
Magnus O. Myreen and
Ramana Kumar and
Anthony Fox and
Scott Owens and
Michael Norrish The verified CakeML compiler backend . . e2
Tom Schrijvers and
Bruno C. D. S. Oliveira and
Philip Wadler and
Koar Marntirosian COCHIS: Stable and coherent implicits e3
Ben Greenman and
Asumu Takikawa and
Max S. New and
Daniel Feltey and
Robert Bruce Findler and
Jan Vitek and
Matthias Felleisen How to evaluate the performance of
gradual type systems . . . . . . . . . . e4
Kwanghoon Choi and
Byeong-Mo Chang A theory of RPC calculi for
client-server model . . . . . . . . . . e5
Olivier Danvy Folding left and right over Peano
numbers . . . . . . . . . . . . . . . . e6
Álvaro García-Pérez and
Pablo Nogueira The full-reducing Krivine abstract
machine KN simulates pure normal-order
reduction in lockstep: A proof via
corresponding calculus . . . . . . . . . e7
Richard S. Bird How to find a fake coin . . . . . . . . e8
Tiark Rompf and
Nada Amin A SQL to C compiler in 500 lines of code e9
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e10
David Darais and
David Van Horn Constructive Galois Connections . . . . e11
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e1
Jesper Cockx and
Andreas Abel Elaborating dependent (co)pattern
matching: No pattern left behind . . . . e2
Richard S. Bird An optimal, purely functional
implementation of the Garsia--Wachs
algorithm . . . . . . . . . . . . . . . e3
J. Hackett Review of ``\booktitleThinking with
Types'' by Sandy Maguire, LeanPub, 2019 e4
Daniel Hillerström and
Sam Lindley and
Robert Atkey Effect handlers via generalised
continuations . . . . . . . . . . . . . e5
Éric Tanter Review of ``\booktitleThe Little
Prover'' by Daniel P. Friedman and Carl
Eastlund, MIT Press, 2015 . . . . . . . e6
Oleg Kiselyov Many more predecessors: A representation
workout . . . . . . . . . . . . . . . . e7
Jonathan Immanuel Brachthäuser and
Philipp Schuster and
Klaus Ostermann Effekt: Capability-passing style for
type- and effect-safe, extensible effect
handlers in Scala . . . . . . . . . . . e8
Lukas Convent and
Sam Lindley and
Conor Mcbride and
Craig Mclaughlin Doo bee doo bee doo . . . . . . . . . . e9
Wouter Swierstra Heterogeneous binary random-access lists e10
Andrey Mokhov and
Neil Mitchell and
Simon Peyton Jones Build systems \`a la carte: Theory and
practice . . . . . . . . . . . . . . . . e11
Ivan Perez and
Alwyn E. Goodloe Fault-tolerant functional reactive
programming (extended version) . . . . . e12
Ziga Luksic and
Matija Pretnar Local algebraic effect theories . . . . e13
Beniamino Accattoli and
Stéphane Graham-Lengrand and
Delia Kesner Tight typings and split bounds, fully
developed . . . . . . . . . . . . . . . e14
Georgios Karachalias and
Matija Pretnar and
Amr Hany Saleh and
Stien Vanderhallen and
Tom Schrijvers Explicit effect subtyping . . . . . . . e15
Jan De Muijnck-Hughes Type-Driven Development with Idris . . . e16
Andreas Abel and
Jesper Cockx and
Dominique Devriese and
Amin Timany and
Philip Wadler Leibniz equality is isomorphic to
Martin-Löf identity, parametrically . . . e17
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e18
Prabhakar Ragde Review of ``\booktitleAlgorithms for
Functional Programming'' by John David
Stone, Springer-Verlag, 2018 . . . . . . e19
Michael Sperber Review of ``\booktitleFunctional and
Reactive Domain Modeling'' by Debasish
Ghosh, Manning, 2017, ISBN
978-1-617-29224-8 . . . . . . . . . . . e21
Ruben P. Pieters and
Tom Schrijvers Faster coroutine pipelines: A
reconstruction . . . . . . . . . . . . . e22
Ruben P. Pieters and
Exequiel Rivas and
Tom Schrijvers Generalized monoidal effects and
handlers . . . . . . . . . . . . . . . . e23
Karl Crary A focused solution to the avoidance
problem . . . . . . . . . . . . . . . . e24
Patrick Bahr and
Graham Hutton Calculating correct compilers II: Return
of the register machines . . . . . . . . e25
Matt Mccutchen and
Judith Borghouts and
Andrew D. Gordon and
Simon Peyton Jones and
Advait Sarkar Elastic sheet-defined functions:
Generalising spreadsheet functions to
variable-size input arrays . . . . . . . e26
Sam Caldwell and
Tony Garnock-Jones and
Matthias Felleisen Typed dataspace actors . . . . . . . . . e27
Ivan Perez and
Henrik Nilsson Runtime verification and validation of
functional reactive systems . . . . . . e28
Torsten Grust Review of ``Algorithm Design with
Haskell'' by Richard Bird and Jeremy
Gibbons, Cambridge University Press,
2020 . . . . . . . . . . . . . . . . . . e29
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e1
Oleg Kiselyov and
Shin-Cheng Mu and
Amr Sabry Not by equations alone: Reasoning with
extensible effects . . . . . . . . . . . e2
Kristoffer Just Arndal Andersen and
Ilya Sergey Protocol combinators for modeling,
testing, and execution of distributed
systems . . . . . . . . . . . . . . . . e3
Martin Elsman and
Niels Hallenberg Integrating region memory management and
tag-free generational garbage collection e4
Joachim Breitner and
Antal Spector-Zabusky and
Yao Li and
Christine Rizkallah and
John Wiegley and
Joshua Cohen and
Stephanie Weirich Ready, Set , Verify! Applying hs-to-coq
to real-world Haskell code . . . . . . . e5
Thomas Van Strydonck and
Frank Piessens and
Dominique Devriese Linear capabilities for fully abstract
compilation of separation-logic-verified
code . . . . . . . . . . . . . . . . . . e6
Akimasa Morihata Lambda calculus with algebraic
simplification for reduction
parallelisation: Extended study . . . . e7
Andrea Vezzosi and
Anders MÖRtberg and
Andreas Abel Cubical Agda: a dependently typed
programming language with univalence and
higher inductive types . . . . . . . . . e8
Lau Skorstengaard and
Dominique Devriese and
Lars Birkedal StkTokens: Enforcing well-bracketed
control flow and stack encapsulation
using linear capabilities . . . . . . . e9
Martin Erwig and
Prashant Kumar Explainable dynamic programming . . . . e10
Jonathan Sterling Higher order functions and Brouwer's
thesis . . . . . . . . . . . . . . . . . e11
Andrzej Filinski Proof-directed program transformation: a
functional account of efficient regular
expression matching . . . . . . . . . . e12
Tomas Petricek Composable data visualizations . . . . . e13
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e14
Jeremy Gibbons How to design co-programs . . . . . . . e15
Shriram Krishnamurthi What is an education paper? . . . . . . e16
Reynald Affeldt and
Jacques Garrigue and
David Nowak and
Takafumi Saikawa A trustful monad for axiomatic reasoning
with probability and nondeterminism . . e17
Robert Sison and
Toby Murray Verified secure compilation for
mixed-sensitivity concurrent programs e18
Bhargav Shivkumar and
Jeffrey Murphy and
Lukasz Ziarek Real-time MLton: a Standard ML runtime
for real-time functional programs . . . e19
Jeremy G. Siek and
Peter Thiemann and
Philip Wadler Blame and coercion: Together again for
the first time . . . . . . . . . . . . . e20
Max S. New and
Daniel R. Licata and
Amal Ahmed Gradual type theory . . . . . . . . . . e21
Guillaume Allais and
Robert Atkey and
James Chapman and
Conor Mcbride and
James Mckinna A type- and scope-safe universe of
syntaxes with binding: their semantics
and proofs . . . . . . . . . . . . . . . e22
Peter Achten Segments: an alternative rainfall
problem . . . . . . . . . . . . . . . . e23
Nicola Botta and
Nuria Brede and
Patrik Jansson and
Tim Richter Extensional equality preservation and
verified generic programming . . . . . . e24
Liam O'Connor and
Zilin Chen and
Christine Rizkallah and
Vincent Jackson and
Sidney Amani and
Gerwin Klein and
Toby Murray and
Thomas Sewell and
Gabriele Keller Cogent: uniqueness types and certifying
compilation . . . . . . . . . . . . . . e25
Nuria Brede and
Nicola Botta On the correctness of monadic backward
induction . . . . . . . . . . . . . . . e26
Weihao Qu and
Marco Gaboardi and
Deepak Garg Relational cost analysis in a
functional-imperative setting . . . . . e27
Xuejing Huang and
Jinxu Zhao and
Bruno C. D. S. Oliveira Taming the Merge Operator . . . . . . . e28
Richard Bird and
Shin-Cheng Mu A greedy algorithm for dropping digits e29
Jeremy G. Siek and
Tianyu Chen Parameterized cast calculi and reusable
meta-theory for gradually typed lambda
calculi . . . . . . . . . . . . . . . . e30
Shin-Cheng Mu and
Tsung-Ju Chiang Longest segment of balanced parentheses:
an exercise in program inversion in a
segment problem . . . . . . . . . . . . e31
Jeremy Gibbons and
Shriram Krishnamurthi Editorial . . . . . . . . . . . . . . . e1
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e2
Derek Dreyer and
Benjamin C. Pierce On being a PhD student of Robert Harper e3
Hideya Iwasaki and
Kento Emoto and
Akimasa Morihata and
Kiminori Matsuzaki and
Zhenjiang Hu Fregel: a functional domain-specific
language for vertex-centric large-scale
graph processing . . . . . . . . . . . . e4
Ralf Hinze and
Colin Runciman Super-naturals . . . . . . . . . . . . . e5
Klaas Pruiksma and
Frank Pfenning Back to futures . . . . . . . . . . . . e6
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e7
Norman Danner and
Daniel R. Licata Denotational semantics as a foundation
for cost recurrence extraction for
functional languages . . . . . . . . . . e8
Stefano Perna and
Val Tannen and
Limsoon Wong Iterating on multiple collections in
synchrony . . . . . . . . . . . . . . . e9
Wouter Swierstra A well-known representation of monoids
and its application to the function
`vector reverse' . . . . . . . . . . . . e10
Danil Annenkov and
Mikkel Milo and
Jakob Botsch Nielsen and
Bas Spitters Extracting functional programs from Coq,
in Coq . . . . . . . . . . . . . . . . . e11
Paulette Koronkevich and
Ramon Rakow and
Amal Ahmed and
William J. Bowman ANF preserves dependent types up to
extensional equality . . . . . . . . . . e12
Olivier Danvy Fold--unfold lemmas for reasoning about
recursive programs using the Coq proof
assistant . . . . . . . . . . . . . . . e13
John Peter Campora Iii and
Sheng Chen and
Martin Erwig and
Eric Walkingshaw Migrating gradual types . . . . . . . . e14
Patrick Bahr Modal FRP for all: Functional reactive
programming without space leaks in
Haskell . . . . . . . . . . . . . . . . e15
Cheng-En Chuang and
Grant Iraci and
Lukasz Ziarek Send to me first: Priority in
synchronous message-passing . . . . . . e16
Graham Hutton PhD Abstracts . . . . . . . . . . . . . e17
Jonathan Chan and
Yufeng Li and
William J. Bowman Is sized typing for Coq practical? . . . ??
Olivier Danvy Folding left and right matters: Direct
style, accumulators, and continuations ??
Olivier Danvy Fold--unfold lemmas for reasoning about
recursive programs using the Coq proof
assistant --- Erratum . . . . . . . . . ??
Paul Downen and
Zena M. Ariola Classical (co)recursion: Mechanics . . . ??
Siddharth Bhaskar and
Jakob Grue Simonsen Read/write factorizable programs . . . . ??
Graham Hutton PhD Abstracts . . . . . . . . . . . . . ??
Jason Z. S. Hu and
Junyoung Jang and
Brigitte Pientka Normalization by evaluation for modal
dependent type theory . . . . . . . . . ??
Martin Sulzmann and
Stefan Wehr A type-directed, dictionary-passing
translation of method overloading and
structural subtyping in Featherweight
Generic Go . . . . . . . . . . . . . . . ??
Graham Hutton Programming language semantics: It's
easy as 1, 2, 3 . . . . . . . . . . . . ??
Hanliang Zhang and
Wenhao Tang and
Ruifeng Xie and
Meng Wang and
Zhenjiang Hu Contract lenses: Reasoning about
bidirectional programs via calculation ??
Wouter Swierstra A correct-by-construction conversion
from lambda calculus to combinatory
logic . . . . . . . . . . . . . . . . . ??
Ralf Hinze Certified, total serialisers with an
application to Huffman encoding . . . . ??
Julia Jansson and
Patrik Jansson Level-$p$-complexity of Boolean
functions using thinning, memoization,
and polynomials . . . . . . . . . . . . ??
Cameron Moy and
Matthias Felleisen Trace contracts . . . . . . . . . . . . ??
Graham Hutton PhD Abstracts . . . . . . . . . . . . . ??
Eva Graversen and
Andrew K. Hirsch and
Fabrizio Montesi Alice or Bob?: Process polymorphism in
choreographies . . . . . . . . . . . . . ??
Kazutaka Matsuda and
Meng Wang Sparcl: A language for partially
invertible computation . . . . . . . . . ??
Cameron Moy Knuth--Morris--Pratt illustrated . . . . ??
Chenghao Su and
Lin Chen and
Li Yanhui and
Yuming Zhou Static Blame for gradual typing . . . . ??
Daniel Hillerström and
Sam Lindley and
John Longley Asymptotic speedup via effect handlers ??
Michael Sperber A review for the \booktitleJournal of
Functional Programming of Sandy Maguire,
\booktitleAlgebra-Driven Design
(Leanpub, 2020) . . . . . . . . . . . . ??
Taro Sekiyama and
Takeshi Tsukada and
Atsushi Igarashi Signature restriction for polymorphic
algebraic effects . . . . . . . . . . . ??