Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Kristian Støvring
[go: Go Back, main page]

Kristian Støvring

Post-doc, FIRST Research School, 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 phone: (+45) 7218 5047
Email: kss (at) brics (dot) dk

Publications

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.
To be presented at ICFP 2007.
Preprint: [ps, pdf]

A Complete, Co-Inductive Syntactic Theory of Sequential Control and State.
With Soren Lassen.
In POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, 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]