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.

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.

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!