The book was completed in May 2023 so I figure this warrants a re-submission. I'm reading through it now if anybody has time and wants to work through it together.
Thread
Stories related to "Functional Programming in Lean" across the full archive.
Formally-Verified Interpreter for a Shell-like, Programming Language (2017)
(hal-univ-diderot.archives-ouvertes.fr)
Abstract: "—In this paper we present loose programming, an approach designed to enable process developers to design their application-specific processes in an intuitive style. Key to this approach is the concept of loose specification, a graphical formalism that allows developers to express their pr...
Slides for the lambdaMTL meetup presentation by John Plaice.
The Abstract State Machines Method for Modular Design and Analysis of Programming Languages (2013)
(pages.di.unipi.it)
Abstract: "We survey the use of Abstract State Machines in the area of programming languages, namely to define behavioral properties of programs at source, intermediate and machine levels in a way that is amenable to mathematical and experimental analysis by practitioners, like correctness and compl...
Abstract: "Program synthesis is the task of automatically finding a program in the
underlying programming language that satisfies the user intent expressed
in the form of some specification. Since the inception of AI in the 1950s,
this problem has been considered the holy grail of Computer Scienc...
Programming and Reasoning with Algebraic Effects and Dependent Types (2013)
(eb.host.cs.st-andrews.ac.uk)
Abstract: "One often cited benefit of pure functional programming is that pure
code is easier to test and reason about, both formally and infor-
mally. However, real programs have side-effects including state
management, exceptions and interactions with the outside world.
Haske...
Abstract: "The
need
for
direct
memory
manipulation
through
pointers
is essential
in
man
y applications.
Ho
we
ver, it is also
commonly
understood
that
the
use
(or
probably
misuse)
of
pointers
is often
a rich
source
of
program
errors.
Therefore,
approaches
that
can
...
I found this page from Cornell University from the Fall of 2017 this morning. While I've done a bit of Haskell and Rust, I've never really gotten into OCaml. Lots of good explanations here.
Towards the end they switch from utilizing OCaml to Coq to introduce formal methods.
Abstract: "There exists an identifiable programming style based on the widespread use of type
information handled through mechanical typechecking techniques.
This
typeful
programming style is in a sense independent of the language it is embedded in; it
adapts equally well to funct...
Abstract: "This tutorial provides a programmer's introduction to the Satisfiability Modulo Theories Solver Z3. It describes how to use Z3 through scripts, provided in the Python scripting language, and it describes several of the algorithms underlying the decision procedures within Z3. It aims to br...
Resource-safe Systems Programming with Embedded Domain Specific Languages
(eb.host.cs.st-andrews.ac.uk)
Abstract: "We introduce a new overloading notation that facilitates programming, modularity and reuse in Embedded Domain Specific Languages (EDSLs), and use it to reason about safe resource usage and state management. We separate the structural language constructs from our primiti...
A Modular Scheme for Deadlock Prevention in an Object-Oriented Programming Model (2010)
(se.inf.ethz.ch)
Abstract: "Despite the advancements of concurrency theory in the past
decades, practical concurrent programming has remained a challenging
activity. Fundamental problems such as data races and deadlocks still
persist for programmers since available detection and prevention tools
are unsound or h...
I've been looking at SPARK Ada after reading comments by users here, since I'm getting into embedded programming but don't want to go back to writing C and C++. There are a number of very confusing things about SPARK Ada, licensing-wise - a cursory glance will lead you to believe it's one of those c...
See also https://whileydave.com/publications/pea22_gpce/