Kristian Støvring

Post-doc in the Programming, Logic, and Semantics group, headed by Lars Birkedal, at the IT University of Copenhagen.

PhD, computer science, University of Aarhus, 2007.
My supervisors were Olivier Danvy and Andrzej Filinski.

Research interests: Programming language semantics, lambda calculus, formalized mathematics.

Contact information:

IT University of Copenhagen
Rued Langgaards Vej 7
DK-2300 Copenhagen S
Denmark

Office: 4C09
Office phone: (+45) 7218 5047
Fax: (+45) 7218 5001
Email: kss (at) itu (dot) dk

Activities

TLDI 2010: PC member.
Visiting Carnegie Mellon University, June–July 2009.
Co-organizer of the FIRST PhD Fall school on Logics and Semantics of State, October 2008.

Publications

Kripke Models over Recursively Defined Metric Worlds: Steps and Domains.
With Lars Birkedal and Jacob Thamsborg.
January 2010. Submitted.
[pdf]

Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types.
With Lars Birkedal and Jacob Thamsborg.
December 2009. Long version, submitted to journal.
[pdf]

A Complete, Co-Inductive Syntactic Theory of Sequential Control and State.
With Soren Lassen. Long version.
In Semantics and Algebraic Specification: Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday, p. 329-375.
Number 5700 in Lecture Notes in Computer Science. August 2009.

The Category-Theoretic Solution of Recursive Metric-Space Equations.
With Lars Birkedal and Jacob Thamsborg.
ITU Tech Report TR-2009-119. Submitted to journal.
Extended abstract presented at the 6th Workshop on Fixed Points in Computer Science, FICS 2009.
[pdf]

Inductive Reasoning about Effectful Data Types.
With Andrzej Filinski.
April 2008. Long version, submitted to journal.

Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types.
With Lars Birkedal and Jacob Thamsborg.
In Proceedings of the Twelfth International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2009, p. 456-470.
[pdf]

Relational Parametricity for References and Recursive Types.
With Lars Birkedal and Jacob Thamsborg.
In Proceedings of the Fourth ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI 2009, p. 91-104.
[pdf]

On Reasoning Equationally: Lambda Calculi and Programs with Computational Effects.
PhD dissertation, BRICS PhD School, Department of Computer Science, University of Aarhus. August 2007.

Inductive Reasoning about Effectful Data Types.
With Andrzej Filinski.
In Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, p. 97-110, October 2007.
Preprint: [ps, pdf]

A Complete, Co-Inductive Syntactic Theory of Sequential Control and State.
With Soren Lassen.
In Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, POPL 2007, p. 161-172, January 2007.
[pdf]

Higher-Order Beta Matching with Solutions in Long Beta-Eta Normal Form.
Nordic Journal of Computing, 13(1-2):117-126, August 2006.
Also available as BRICS tech report RS-06-12.

Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative.
Logical Methods in Computer Science, 2(2:1):1-14, March 2006.
Download: [ps, pdf]. There is also a formal proof.

Program Extraction from Proofs of Weak Head Normalization.
With Małgorzata Biernacka and Olivier Danvy.
Presented at MFPS XXI, Birmingham, UK, May 2005.
Electronic Notes in Theoretical Computer Science, 155:169-189, May 2006.
Preprint: [ps, pdf]

Teaching

Fall 2009: Programming Workshop.
Spring 2008: Performance and Test.