Journal of Functional Programming

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.

Brent Yorgey reviews Vitaly Bragilevsky's book, "Haskell in Depth"

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!