Concrete Syntax for Data Objects in Functional Languages. - Annika Aasa; Kent Petersson; Dan Synek (LISP and Functional Programming, 1988)

A Set Constructor for Inductive Sets in Martin-Löf's Type Theory. - Kent Petersson; Dan Synek (Category Theory and Computer Science, 1989)

On Generating unique Names. - Lennart Augustsson; Mikael Rittri; Dan Synek (J. Funct. Program., 1994)

Automated Machine-Checked Hybrid System Safety Proofs. - Herman Geuvers; Adam Koprowski; Dan Synek; Eelis van der Weegen (ITP, 2010)