Journal of Functional Programming
@journal-of-fp.bsky.social
Design, implementation & application of functional programming languages from mathematical theory to industrial practice. Posts by @liamoc.net
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.
Program Calculation
Welcome to Cambridge Core
tinyurl.com
November 11, 2025 at 11:42 PM
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.
Call-by-value and call-by-name: A simple proof of a classic theorem | Journal of Functional Programming | Cambridge Core
Call-by-value and call-by-name: A simple proof of a classic theorem - Volume 35
www.cambridge.org
November 4, 2025 at 5:39 AM
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.
Tail recursion modulo context: An equational approach (extended version) | Journal of Functional Programming | Cambridge Core
Tail recursion modulo context: An equational approach (extended version) - Volume 35
www.cambridge.org
November 4, 2025 at 5:36 AM
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.
Automatically testing console I/O behavior of student submissions in Haskell | Journal of Functional Programming | Cambridge Core
Automatically testing console I/O behavior of student submissions in Haskell - Volume 35
www.cambridge.org
September 16, 2025 at 12:07 AM
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!
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!
PhD Abstracts | Journal of Functional Programming | Cambridge Core
PhD Abstracts - Volume 35
www.cambridge.org
August 10, 2025 at 10:07 AM
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!
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!
OCaml Blockly | Journal of Functional Programming | Cambridge Core
OCaml Blockly - Volume 35
www.cambridge.org
August 10, 2025 at 10:01 AM
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.
Binary search—think positive | Journal of Functional Programming | Cambridge Core
Binary search—think positive - Volume 35
www.cambridge.org
August 10, 2025 at 9:59 AM
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.
The graphical theory of monads | Journal of Functional Programming | Cambridge Core
The graphical theory of monads - Volume 35
www.cambridge.org
August 10, 2025 at 9:55 AM
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.
Domain-specific tensor languages | Journal of Functional Programming | Cambridge Core
Domain-specific tensor languages - Volume 35
www.cambridge.org
August 10, 2025 at 9:52 AM
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.
Recursive subtyping for all | Journal of Functional Programming | Cambridge Core
Recursive subtyping for all - Volume 35
www.cambridge.org
March 1, 2025 at 10:33 AM
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.
How much is in a square? Calculating functional programs with squares | Journal of Functional Programming | Cambridge Core
How much is in a square? Calculating functional programs with squares - Volume 35
www.cambridge.org
March 1, 2025 at 10:26 AM
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"
Review of “Haskell in Depth” by Vitaly Bragilevsky, Manning Publications, 2021 | Journal of Functional Programming | Cambridge Core
Review of “Haskell in Depth” by Vitaly Bragilevsky, Manning Publications, 2021 - Volume 35
www.cambridge.org
February 17, 2025 at 5:08 AM
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.
Experiences of early assessment to teach functional programming | Journal of Functional Programming | Cambridge Core
Experiences of early assessment to teach functional programming - Volume 35
www.cambridge.org
February 7, 2025 at 11:52 PM
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.
Turner, Bird, Eratosthenes: An eternal burning thread | Journal of Functional Programming | Cambridge Core
Turner, Bird, Eratosthenes: An eternal burning thread - Volume 35
www.cambridge.org
February 7, 2025 at 11:50 PM
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.
You could have invented Fenwick trees | Journal of Functional Programming | Cambridge Core
You could have invented Fenwick trees - Volume 35
www.cambridge.org
January 24, 2025 at 2:05 PM
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.
A practical formalization of monadic equational reasoning in dependent-type theory | Journal of Functional Programming | Cambridge Core
A practical formalization of monadic equational reasoning in dependent-type theory - Volume 35
www.cambridge.org
January 13, 2025 at 3:28 AM
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!
PhD Abstracts | Journal of Functional Programming | Cambridge Core
PhD Abstracts - Volume 35
www.cambridge.org
January 13, 2025 at 3:23 AM
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.
From high to low: Simulating nondeterminism and state with state | Journal of Functional Programming | Cambridge Core
From high to low: Simulating nondeterminism and state with state - Volume 34
www.cambridge.org
January 13, 2025 at 3:15 AM
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.
A simple blame calculus for explicit nulls | Journal of Functional Programming | Cambridge Core
A simple blame calculus for explicit nulls - Volume 34
www.cambridge.org
January 3, 2025 at 2:17 PM
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.
An example of goal-directed, calculational proof | Journal of Functional Programming | Cambridge Core
An example of goal-directed, calculational proof - Volume 34
www.cambridge.org
December 16, 2024 at 4:27 AM
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.
Bottom-up computation using trees of sublists | Journal of Functional Programming | Cambridge Core
Bottom-up computation using trees of sublists - Volume 34
www.cambridge.org
December 16, 2024 at 4:21 AM
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.
Programming and reasoning about actors that share state | Journal of Functional Programming | Cambridge Core
Programming and reasoning about actors that share state - Volume 34
www.cambridge.org
December 6, 2024 at 2:09 PM
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!
November 13, 2024 at 2:02 PM
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!