Explaining ML Type Errors by Data Flows. - Holger Gast (IFL, 2004)

A generator for type checkers. - Holger Gast (2004)

Patterns and traceability in teaching software architecture. - Holger Gast (PPPJ, 2008)

Lightweight Separation. - Holger Gast (TPHOLs, 2008)

Managing Proof Documents for Asynchronous Processing. - Holger Gast (UITP@TPHOLs, 2008)

High-level Proofs about Low-level Programs. - Holger Gast; Julia Trieflinger (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2009)

A Developer-oriented Hoare Logic. - Holger Gast (PSPL@LICS, 2010)

Engineering the Prover Interface. - Holger Gast (UITP, 2010)

Reasoning about memory layouts. - Holger Gast (Formal Methods Syst. Des., 2010)

Developer-Oriented Correctness Proofs - A Case Study of Cheney's Algorithm. - Holger Gast (ICFEM, 2011)

Structuring Interactive Correctness Proofs by Formalizing Coding Idioms. - Holger Gast (SSV, 2011)

Semi-automatic Proofs about Object Graphs in Separation Logic. - Holger Gast (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012)