We're delighted to announce that the JFP Special Issue on Program Calculation is now complete, and contains eleven papers that are freely available to read online from the link below.
Biernacki, McKinna and Sieczkowski present a simple new proof of the classic theorem that call-by-value evaluation can be simulated by call-by-name evaluation.
From Daan Leijen and Anton Lorenzen: an extended version of their POPL 2023 paper, "Tail Recursion Modulo Context: An Equational Approach", which calculates a generalisation of the "tail recursion modulo cons" optimisation from its specification.
Oliver Westphal and Janis Voigtländer present a formal specification language and automated testing framework for the console I/O behaviour of student-submitted programs.
Last month we published our PhD abstracts in FP from the last year.
Congratulations to Fahad Alhabardi, Colm Baston, Daniel Britten, Joris Ceulemans, Lawrence Dunn, Yuning Feng, Kiran Gopinathan, Sebastian Graf, Jason Z. S. Hu, Joomy Korkut, Daniele Pautasso and Jui-Hsuan Wu!
In Education Matters, Kenichi Asai presents OCaml Blockly -- an educational block-based programming environment for beginners, like Google Blockly -- but for OCaml!
Alexander Dinges and Ralf Hinze present a dramatic pearl about binary search with Agda.
Ralf Hinze and Dan Marsden present a graphical calculational technique based on string diagrams, and use it to explain the theory of monads.
J.P. Bernardy and P. Jansson present a new Haskell-embedded domain specific language for naturally expressing tensor computations using natural index notation.
Litao Zhou, Yaoda Zhou, Qianyong Wan and Bruno C.D.S. Oliveira present a new core calculus that extends F_≤ (a well known polymorphic calculus with bounded quantification) with isorecursive types, tackling the tricky combination of subtyping, recursive types, and bounded quantification.
José Nuno Oliveira writes this pearl exploring "magic squares" --- (semi-)commutative squares. These squares underpin much of what we do in logic, FP, database modelling, formal semantics and so on.
In Education Matters, Peter Chapman reports on the use of Use-Modify-Create scaffolds to teach first-year undergraduate functional programming. This early assessment intervention showed promising improvements to student scores.
Read Jeremy Gibbons' pearl exploring Richard Bird's Sieve of Eratosthenes circular algorithm through the lens of Turner's Total Functional Programming.
Read Brent Yorgey's functional pearl calculating an efficient implementation of Fenwick trees from a straightforward, purely functional segment tree.
In this paper, Reynald Affeldt, Jacques Garrigue and Takafumi Saikawa present a framework embedded inside Rocq for practical equational reasoning about programs with effects using a formalisation of a hierarchy of effects.
Congratulations to Pedro Jorge Fernandes Ângelo, Leonhard Applis, Thiago Felicissimo, Matthías Páll Gissurarson, Harrison Goldstein, Brandon Hewer, Jack Hughes, Eddie Jones, Jesse Sigal, and James Wood!
We're delighted to publish ten PhD abstracts in this round. Topics range from types to tests, from synthesis to software engineering, from datatypes to differentiation. Have a look!
Read Wenhao Tang and Tom Schrijvers' paper on simulating nondeterminism and state (high level effects) in terms of low-level state, proving each step of the refinement correct by program calculation.
New paper: Lhoták and Wadler present a simpler blame calculus for gradual typing of languages where types explicitly indicate whether null values are permitted.
Speaking of pearls, we also have Backhouse, Guttmann and Winter's pearl, showing a neat example of a goal-directed, calculational proof: constructing an equivalence relation from a given relation by way of a starth root construction.
Have a read of Shin-Cheng Mu's beautiful functional pearl on deriving an algorithm for bottom-up computation using trees of sublists.
New Paper: Caldwell, Garnock-Jones and Felleisen allow programmers to state temporal aspects of actor conversations in dataspace actor languages. They present a design of a language of _facets_ and a system for reasoning about their temporal behaviour.
I've set up a bluesky account for the Journal of Functional Programming. Please follow for all our latest papers, news about special issues, and other announcements!
