Lawrence Paulson
@lawrpaulson.bsky.social
Computer scientist with a background in mathematics and logic. Academic researching formal verification technologies and applications.
Reposted by Lawrence Paulson
The UK, where the day after a decision to take half a million children out of poverty, the media & political world has been full of sneering at those same children & their families, labelling them as ‘Benefits Street’, while the same people are moaning about a tax on £2m mansions. Shameful stuff.
November 27, 2025 at 8:22 PM
The UK, where the day after a decision to take half a million children out of poverty, the media & political world has been full of sneering at those same children & their families, labelling them as ‘Benefits Street’, while the same people are moaning about a tax on £2m mansions. Shameful stuff.
Just out: Functional Data Structures, edited by Tobias Nipkow
November 25, 2025 at 12:48 PM
Just out: Functional Data Structures, edited by Tobias Nipkow
The Weak Spectroscopy Game to Characterize Behavioral Equivalences
Lisa Barthel et al
We formalise Bisping and Jansen's weak spectroscopy game, which can be used to characterize and decide a hierarchy of behavioral equivalences for systems with internal behavior.
www.isa-afp.org/entries/Weak...
Lisa Barthel et al
We formalise Bisping and Jansen's weak spectroscopy game, which can be used to characterize and decide a hierarchy of behavioral equivalences for systems with internal behavior.
www.isa-afp.org/entries/Weak...
The Weak Spectroscopy Game to Characterize Behavioral Equivalences
The Weak Spectroscopy Game to Characterize Behavioral Equivalences in the Archive of Formal Proofs
www.isa-afp.org
November 22, 2025 at 11:23 AM
The Weak Spectroscopy Game to Characterize Behavioral Equivalences
Lisa Barthel et al
We formalise Bisping and Jansen's weak spectroscopy game, which can be used to characterize and decide a hierarchy of behavioral equivalences for systems with internal behavior.
www.isa-afp.org/entries/Weak...
Lisa Barthel et al
We formalise Bisping and Jansen's weak spectroscopy game, which can be used to characterize and decide a hierarchy of behavioral equivalences for systems with internal behavior.
www.isa-afp.org/entries/Weak...
Rely-Guarantee Extensions and Locks
RJ Colvin et al
We extend the existing rely-guarantee library with flexible syntax, data-invariant support, etc.
We apply our library to three queue locks: the
Abstract Queue Lock, the Ticket Lock, and the Circular Buffer Lock.
www.isa-afp.org/entries/RG_L...
RJ Colvin et al
We extend the existing rely-guarantee library with flexible syntax, data-invariant support, etc.
We apply our library to three queue locks: the
Abstract Queue Lock, the Ticket Lock, and the Circular Buffer Lock.
www.isa-afp.org/entries/RG_L...
Rely-Guarantee Extensions and Locks
Rely-Guarantee Extensions and Locks in the Archive of Formal Proofs
www.isa-afp.org
November 21, 2025 at 5:06 PM
Rely-Guarantee Extensions and Locks
RJ Colvin et al
We extend the existing rely-guarantee library with flexible syntax, data-invariant support, etc.
We apply our library to three queue locks: the
Abstract Queue Lock, the Ticket Lock, and the Circular Buffer Lock.
www.isa-afp.org/entries/RG_L...
RJ Colvin et al
We extend the existing rely-guarantee library with flexible syntax, data-invariant support, etc.
We apply our library to three queue locks: the
Abstract Queue Lock, the Ticket Lock, and the Circular Buffer Lock.
www.isa-afp.org/entries/RG_L...
Discrete Upper Confidence Bound Algorithm in HOL
by A Faber
He formally verifies the Discrete Upper Confidence Bound (UCB) algorithm, focusing on its probabilistic guarantees and regret bounds. The work explores verification of discrete-time bandit models.
www.isa-afp.org/entries/Disc...
by A Faber
He formally verifies the Discrete Upper Confidence Bound (UCB) algorithm, focusing on its probabilistic guarantees and regret bounds. The work explores verification of discrete-time bandit models.
www.isa-afp.org/entries/Disc...
Discrete Upper Confidence Bound Algorithm in HOL
Discrete Upper Confidence Bound Algorithm in HOL in the Archive of Formal Proofs
www.isa-afp.org
November 20, 2025 at 2:22 PM
Discrete Upper Confidence Bound Algorithm in HOL
by A Faber
He formally verifies the Discrete Upper Confidence Bound (UCB) algorithm, focusing on its probabilistic guarantees and regret bounds. The work explores verification of discrete-time bandit models.
www.isa-afp.org/entries/Disc...
by A Faber
He formally verifies the Discrete Upper Confidence Bound (UCB) algorithm, focusing on its probabilistic guarantees and regret bounds. The work explores verification of discrete-time bandit models.
www.isa-afp.org/entries/Disc...
Pre*: The Predecessors of a Regular Language wrt a Context-Free Grammar
T Lemke & T Nipkow
Let L be a language, G a cfg and Pre*(L) the set of all predecessors of words in L. If L is regular so is Pre*(L). We formalize 2 algorithms to compute Pre*(L) for regular L.
www.isa-afp.org/entries/Pre_...
T Lemke & T Nipkow
Let L be a language, G a cfg and Pre*(L) the set of all predecessors of words in L. If L is regular so is Pre*(L). We formalize 2 algorithms to compute Pre*(L) for regular L.
www.isa-afp.org/entries/Pre_...
Pre*: The Predecessors of a Regular Language w.r.t. a Context-Free Grammar, with Applications
Pre*: The Predecessors of a Regular Language w.r.t. a Context-Free Grammar, with Applications in the Archive of Formal Proofs
www.isa-afp.org
November 19, 2025 at 11:30 AM
Pre*: The Predecessors of a Regular Language wrt a Context-Free Grammar
T Lemke & T Nipkow
Let L be a language, G a cfg and Pre*(L) the set of all predecessors of words in L. If L is regular so is Pre*(L). We formalize 2 algorithms to compute Pre*(L) for regular L.
www.isa-afp.org/entries/Pre_...
T Lemke & T Nipkow
Let L be a language, G a cfg and Pre*(L) the set of all predecessors of words in L. If L is regular so is Pre*(L). We formalize 2 algorithms to compute Pre*(L) for regular L.
www.isa-afp.org/entries/Pre_...
Reposted by Lawrence Paulson
Sometimes, a front page can sum up quite a lot that’s wrong with the world. Including the paper itself which has been so complicit in getting us to a place where children born to refugees could be deported, Trump celebrates despotic wealth and Boris Johnson’s sister moans about not being rich. Ugh.
November 19, 2025 at 7:40 AM
Sometimes, a front page can sum up quite a lot that’s wrong with the world. Including the paper itself which has been so complicit in getting us to a place where children born to refugees could be deported, Trump celebrates despotic wealth and Boris Johnson’s sister moans about not being rich. Ugh.
New in the AFP: Formalizing Neural Networks
A Brucker & A Stell
The use of deep learning is constrained by the lack of verification techniques. We address this issue by formalizing an important class of neural networks, feed-forward neural networks, in Isabelle.
www.isa-afp.org/entries/Neur...
A Brucker & A Stell
The use of deep learning is constrained by the lack of verification techniques. We address this issue by formalizing an important class of neural networks, feed-forward neural networks, in Isabelle.
www.isa-afp.org/entries/Neur...
Formalizing Neural Networks
Formalizing Neural Networks in the Archive of Formal Proofs
www.isa-afp.org
November 17, 2025 at 6:31 PM
New in the AFP: Formalizing Neural Networks
A Brucker & A Stell
The use of deep learning is constrained by the lack of verification techniques. We address this issue by formalizing an important class of neural networks, feed-forward neural networks, in Isabelle.
www.isa-afp.org/entries/Neur...
A Brucker & A Stell
The use of deep learning is constrained by the lack of verification techniques. We address this issue by formalizing an important class of neural networks, feed-forward neural networks, in Isabelle.
www.isa-afp.org/entries/Neur...
A new version of a talk I've given many times: formalising the Diagonal Ramsey paper
youtu.be/YO-LUhUxtFc
youtu.be/YO-LUhUxtFc
Diagonal Ramsey
YouTube video by Lawrence Paulson
youtu.be
November 14, 2025 at 12:35 PM
A new version of a talk I've given many times: formalising the Diagonal Ramsey paper
youtu.be/YO-LUhUxtFc
youtu.be/YO-LUhUxtFc
New on my blog: "Why don't you use dependent types?"
lawrencecpaulson.github.io/2025/11/02/W...
lawrencecpaulson.github.io/2025/11/02/W...
"Why don't you use dependent types?"
lawrencecpaulson.github.io
November 2, 2025 at 11:44 AM
New on my blog: "Why don't you use dependent types?"
lawrencecpaulson.github.io/2025/11/02/W...
lawrencecpaulson.github.io/2025/11/02/W...
New in the AFP: Path Equivalence and Automation for Integration Contours
by M Eberl
Formalises concepts to ease manipulation of paths. Provides the path tactic, which simplifies some proof obligations for composite paths, eg decomposing integrals on a composite path.
www.isa-afp.org/entries/Path...
by M Eberl
Formalises concepts to ease manipulation of paths. Provides the path tactic, which simplifies some proof obligations for composite paths, eg decomposing integrals on a composite path.
www.isa-afp.org/entries/Path...
Path Equivalence and Automation for Integration Contours
Path Equivalence and Automation for Integration Contours in the Archive of Formal Proofs
www.isa-afp.org
October 25, 2025 at 11:53 AM
New in the AFP: Path Equivalence and Automation for Integration Contours
by M Eberl
Formalises concepts to ease manipulation of paths. Provides the path tactic, which simplifies some proof obligations for composite paths, eg decomposing integrals on a composite path.
www.isa-afp.org/entries/Path...
by M Eberl
Formalises concepts to ease manipulation of paths. Provides the path tactic, which simplifies some proof obligations for composite paths, eg decomposing integrals on a composite path.
www.isa-afp.org/entries/Path...
