Supervisors: Olivier Danvy and Andrzej Filinski.
Research interests: Programming language semantics, lambda calculus, formalized mathematics.
Contact information:
BRICS
Department of Computer Science
University of Aarhus
IT-parken, Aabogade 34
DK-8200 Aarhus N
Denmark
Office: Turing.127
Office phone: (+45) 89425783
Email: kss (at) brics (dot) dk
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]