Logic in Computer Science: Modelling and Reasoning About Systems by Michael Huth and Mark Ryan, second edition. ISBN 0 521 54310 X. - Gergely Buday (J. Funct. Program., 2008)

Formalising the SECD machine with nominal Isabelle. - Gergely Buday (SAC, 2015)

Isomorphic Transfer Infrastructure for Nested Types in Isabelle/HOL (Work in Progress). - Gergely Buday; Andrei Popescu 001 (PhD@IFM, 2024)

Countable Sums and Discrete (Sub)Distributions. - Gergely Buday; Andrei Popescu 001 (Arch. Formal Proofs, 2024)