Jan Schwinghammer: Publications

Programming Systems

Jan Schwinghammer

Publications

Teaching

Contact

Here's my entry in the DBLP Bibliography server.

Here's a link to the publications page of the Programming Systems Lab.

Drafts

First steps in synthetic guarded domain theory: step-indexing in the topos of trees   (pdf)
Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, Kristian Støvring
Revised and expanded version of LICS'11 paper. December 2011.

Step-indexed Relational Reasoning for Countable Nondeterminism   (pdf)
Jan Schwinghammer, Lars Birkedal
Revised and expanded version of CSL'11 paper. February 2012.

Journal, conference and workshop publications

A Step-indexed Kripke Model of Hidden State   (pdf)
Jan Schwinghammer, Lars Birkedal, François Pottier, Bernhard Reus, Kristian Støvring, Hongseok Yang
Mathematical Structures in Computer Science, 2012. To appear.

Nested Hoare Triples and Frame Rules for Higher-Order Store   (pdf)
Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang
Logical Methods in Computer Science, 2011.

Step-indexed Relational Reasoning for Countable Nondeterminism   (pdf)
Jan Schwinghammer, Lars Birkedal
Computer Science Logic (CSL'11), 2011.

First steps in synthetic guarded domain theory: step-indexing in the topos of trees   (pdf)
Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, Kristian Støvring
Logic in Computer Science (LICS'11), 2011.

A Step-indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces   (pdf)
Jan Schwinghammer, Lars Birkedal, Kristian Støvring
Foundations of Software Science and Computation Structures (FOSSACS'11), 2011.
A preliminary version of this paper has been presented at the 7th Workshop on Fixed Points in Computer Science, FICS 2010.

Step-indexed Kripke Models over Recursive Worlds   (pdf)
Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, Hongseok Yang
Principles of Programming Languages (POPL'11), 2011

A Metric Model of Lambda Calculus with Guarded Recursion   (pdf)
Lars Birkedal, Jan Schwinghammer, Kristian Støvring
7th Workshop on Fixed Points in Computer Science (FICS'10), 2010.

A Semantic Foundation for Hidden State   (pdf)
Jan Schwinghammer, Hongseok Yang, Lars Birkedal, François Pottier, Bernhard Reus
Foundations of Software Science and Computation Structures (FOSSACS'10), 2010.

Nested Hoare Triples and Frame Rules for Higher-Order Store   (pdf)
Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang
Computer Science Logic (CSL'09), 2009.
Superseded by LMCS article.

Correctly Translating Concurrency Primitives   (pdf)
Jan Schwinghammer, David Sabel, Manfred Schmidt-Schauß, Joachim Niehren
ACM SIGPLAN Workshop on ML (ML'09), 2009.
Based on earlier technical reports TR Frank-34 and TR Frank-37.

Formalizing a Strong Normalization Proof for Moggi's Computational Metalanguage   (pdf)
Christian Doczkal, Jan Schwinghammer
4th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP'09), 2009.

A Step-indexed Semantics of Imperative Objects   (pdf)
Catalin Hritcu, Jan Schwinghammer
Logical Methods in Computer Science, 2009.
An earlier version has been presented at the Foundations of Object-Oriented Languages (FOOL'08) workshop, with full proofs appearing in this technical report.

Coherence of Subsumption for Monadic Types   (pdf)
Jan Schwinghammer
Journal of Functional Programming, 2009.

Adequacy of Compositional Translations for Observational Semantics   (pdf)
Manfred Schmidt-Schauß, Joachim Niehren, David Sabel, Jan Schwinghammer
5th IFIP International Conference on Theoretical Computer Science, 2008.
There is a revised and extended version available.

A Simple Model of Separation Logic for Higher-order Store   (pdf)
Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Hongseok Yang
Int. Conference Automata Logic and Programming (ICALP'08), 2008.

On Normalization by Evaluation for Object Calculi   (pdf)
Jan Schwinghammer
TYPES'07, 2008.

Observational Semantics for a Concurrent Lambda Calculus with Reference Cells and Futures   (pdf)
Joachim Niehren, David Sabel, Manfred Schmidt-Schauß, Jan Schwinghammer
23rd Conference on Mathematical Foundations of Programming Semantics (MFPS XXIII), 2007.
Based on earlier technical report TR Frank-26.

Separation Logic for Higher-order Store   (pdf)
Bernhard Reus, Jan Schwinghammer
Computer Science Logic (CSL'06), 2006.

A Concurrent Lambda Calculus with Futures   (pdf)
Joachim Niehren, Jan Schwinghammer, Gert Smolka
Theoretical Computer Science, 2006.

Denotational Semantics for a Program Logic of Objects   (pdf)
Bernhard Reus, Jan Schwinghammer
Mathematical Structures in Computer Science, 2006.

Denotational Semantics for Abadi and Leino's Logic of Objects   (pdf)
Bernhard Reus, Jan Schwinghammer
The European Symposium on Programming (ESOP'05), 2005.
Superseded by MSCS journal version.

A Typed Semantics of Higher-Order Store and Subtyping   (pdf)
Jan Schwinghammer
Italian Conference on Theoretical Computer Science (ICTCS'05), 2005.

A Concurrent Lambda Calculus with Futures   (pdf)
Joachim Niehren, Jan Schwinghammer, Gert Smolka
5th International Workshop on Frontiers in Combining Systems, 2005.
Superseded by TCS journal version.

Efficiently Computing the Density of Regular Languages
Manuel Bodirsky, Tobias Gärtner, Timo von Oertzen, Jan Schwinghammer
LATIN 2004: Theoretical Informatics: 6th Latin American Symposium, 2004.

Theses

Reasoning about Denotations of Recursive Objects   (pdf)
Jan Schwinghammer
PhD Thesis, Department of Informatics, University of Sussex, 2006.

A Concurrent Lambda-Calculus with Promises and Futures   (pdf)
Jan Schwinghammer
Master's Thesis, Programming Systems Lab, Universität des Saarlandes, 2002.
Awarded the Günter Hotz-Medal for outstanding Computer Science graduates.