Verified programming of Turing machines in Coq. - Yannick Forster 002; Fabian Kunze; Maxi Wuttke (CPP, 2020)

A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. - Yannick Forster 002; Fabian Kunze; Gert Smolka; Maxi Wuttke (ITP, 2021)