constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
(…)
Haskell (in type theory)
Coq, Agda (in dependent type theory)
Quipper (for quantum computation)
Textbook accounts:
Simon Thompson, Haskell: the Craft of Functional Programming, Addison-Wesley (1996) [webpage, pdf]
(with examples in Haskell)
Guy Cousineau, Michel Mauny, The Functional Approach to Programming, Cambridge University Press (2012) [doi:10.1017/CBO9781139173018]
Sergei Winitzki, The Science of Functional Programming – A tutorial, with examples in Scala [leanpub:sofp]
(with examples in Scala)
and with emphasis on the relation to type theory:
Exposition of the categorical semantics of functional programming (such as via monads in computer science):
Bartosz Milewski (compiled by Igal Tabachnik), Category Theory for Programmers, Blurb (2019) [pdf, github, webpage, ISBN:9780464243878]
Bartosz Milewski, The Dao of Functional Programming (2023) [pdf, github]
See also:
Wikipedia, Functional programming
John Backus, Can programming be liberated from the von Neumann style? A functional style and its algebra of programs, Communications of the ACM Volume 21 Number 8, 1978 (pdf)
G. Cousineau, P.-L. Curien, M. Mauny, The Categorical Abstract Machine, Science of Computer Programming 8, 1987 (pdf)
Erik Meijer, Maarten Fokkinga, Ross Paterson, Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire, 1991 (doi:10.1.1.41.125)
Eugenio Moggi, Notions of computations and monads, 1991 (pdf)
David R. Cok, Reasoning about functional programming in Java and C++, ISSTA ‘18: Companion Proceedings for the ISSTA/ECOOP 2018 WorkshopsJuly 2018 Pages 37–39 (doi:10.1145/3236454.3236483)
(building functional programming into imperative programming languages)
Discussion of aspects of quantum computing in terms of monads in functional programming are in
Last revised on September 27, 2023 at 10:20:33. See the history of this page for a list of all contributions to it.