Program Extraction From Proofs of Weak Head Normalization. - Malgorzata Biernacka; Olivier Danvy; Kristian Støvring (MFPS, 2005)

Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative. - Kristian Støvring (Log. Methods Comput. Sci., 2006)

Higher-Order Beta Matching with Solutions in Long Beta-Eta Normal Form. - Kristian Støvring (Nord. J. Comput., 2006)

Inductive reasoning about effectful data types. - Andrzej Filinski; Kristian Støvring (ICFP, 2007)

A Complete, Co-inductive Syntactic Theory of Sequential Control and State. - Kristian Støvring; Søren B. Lassen (Semantics and Algebraic Specification, 2009)

Solutions of Generalized Recursive Metric-Space Equations. - Lars Birkedal; Kristian Støvring; Jacob Thamsborg (FICS, 2009)

Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types. - Lars Birkedal; Kristian Støvring; Jacob Thamsborg (FoSSaCS, 2009)

Relational parametricity for references and recursive types. - Lars Birkedal; Kristian Støvring; Jacob Thamsborg (TLDI, 2009)

A Metric Model of Lambda Calculus with Guarded Recursion. - Lars Birkedal; Jan Schwinghammer; Kristian Støvring (FICS, 2010)

Realisability semantics of parametric polymorphism, general references and recursive types. - Lars Birkedal; Kristian Støvring; Jacob Thamsborg (Math. Struct. Comput. Sci., 2010)

The category-theoretic solution of recursive metric-space equations. - Lars Birkedal; Kristian Støvring; Jacob Thamsborg (Theor. Comput. Sci., 2010)

A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces. - Jan Schwinghammer; Lars Birkedal; Kristian Støvring (FoSSaCS, 2011)

Step-indexed kripke models over recursive worlds. - Lars Birkedal; Bernhard Reus; Jan Schwinghammer; Kristian Støvring; Jacob Thamsborg; Hongseok Yang (POPL, 2011)

Step-Indexed Kripke Model of Separation Logic for Storable Locks. - Alexandre Buisse; Lars Birkedal; Kristian Støvring (MFPS, 2011)

First steps in synthetic guarded domain theory: step-indexing in the topos of trees - Lars Birkedal; Rasmus Ejlers Møgelberg; Jan Schwinghammer; Kristian Støvring (Log. Methods Comput. Sci., 2012)

A relational realizability model for higher-order stateful ADTs. - Lars Birkedal; Kristian Støvring; Jacob Thamsborg (J. Log. Algebraic Methods Program., 2012)

A step-indexed Kripke model of hidden state. - Jan Schwinghammer; Lars Birkedal; François Pottier; Bernhard Reus; Kristian Støvring; Hongseok Yang (Math. Struct. Comput. Sci., 2013)