Step-indexed Relational Reasoning for Countable Nondeterminism
(pdf)
Jan Schwinghammer, Lars Birkedal
Submitted
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
Logical Methods in Computer Science
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
Step-indexed Relational Reasoning for Countable Nondeterminism
(pdf)
Jan Schwinghammer, Lars Birkedal
Computer Science Logic (CSL'11)
Nested Hoare Triples and Frame Rules for Higher-order Store
Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang
Logical Methods in Computer Science
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)
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)
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)
Correctness of Program Translations for Observational Semantics
(pdf)
Manfred Schmidt-Schauß, David Sabel, Joachim Niehren, Jan Schwinghammer
Draft
A Step-indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces
(pdf)
Lars Birkedal, Jan Schwinghammer, Kristian Støvring
Fixed Points in Computer Science (FICS'10)
A Metric Model of Lambda Calculus with Guarded Recursion
(pdf)
Lars Birkedal, Jan Schwinghammer, Kristian Støvring
Fixed Points in Computer Science (FICS'10)
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 2010)
Correctly Translating Concurrency Primitives
(pdf)
Jan Schwinghammer, David Sabel, Manfred Schmidt-Schauß, Joachim Niehren
2009 ACM SIGPLAN Workshop on ML (ML'09)
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)
Nested Hoare Triples and Frame Rules for Higher-Order Store
(pdf)
Jan Schwinghammer, Lars Birkedal, Bernhard Reus, Hongseok Yang
Computer Science Logic (CSL'09)
On Correctness of Buffer Implementations in a Concurrent Lambda Calculus with Futures
(pdf)
Jan Schwinghammer, David Sabel, Joachim Niehren, Manfred Schmidt-Schauß
Technical Report
A Step-indexed Semantics of Imperative Objects
Catalin Hritcu, Jan Schwinghammer
Logical Methods in Computer Science
Coherence of Subsumption for Monadic Types
(pdf)
Jan Schwinghammer
Journal of Functional Programming
On Proving the Equivalence of Concurrency Primitives
(pdf)
Jan Schwinghammer, David Sabel, Joachim Niehren, Manfred Schmidt-Schauß
Technical Report
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
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)
On Normalization by Evaluation for Object Calculi
(pdf)
Jan Schwinghammer
TYPES'07
A Step-indexed Semantics of Imperative Objects (Extended Abstract)
(pdf)
Catalin Hritcu, Jan Schwinghammer
Workshop Proceedings Foundations of Object-Oriented Languages (FOOL'08)
A Proof of Strong Normalization for Call-by-push-value
(pdf)
Christian Doczkal, Jan Schwinghammer
A Step-indexed Semantics of Imperative Objects (Extended Version)
(pdf)
Catalin Hritcu, Jan Schwinghammer
Technical Report
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)
Program Equivalence for a Concurrent Lambda Calculus with Futures
(pdf)
Joachim Niehren, David Sabel, Manfred Schmidt-Schauß, Jan Schwinghammer
Technical Report, Revised version appeared Proc. of Mathematical Foundations of Programming Semantics (23rd MFPS), April 2007
Reasoning about Denotations of Recursive Objects
(pdf)
Jan Schwinghammer
PhD Thesis, Department of Informatics, University of Sussex
Separation Logic for Higher-order Store
(pdf)
Bernhard Reus, Jan Schwinghammer
Computer Science Logic (CSL'06)
A Concurrent Lambda Calculus with Futures
(pdf)
Joachim Niehren, Jan Schwinghammer, Gert Smolka
Theoretical Computer Science
Denotational Semantics for a Program Logic of Objects
(pdf)
Bernhard Reus, Jan Schwinghammer
Mathematical Structures in Computer Science
Denotational Semantics for Abadi and Leino's Logic of Objects
(pdf)
Bernhard Reus, Jan Schwinghammer
The European Symposium on Programming (ESOP'05)
A Typed Semantics of Higher-Order Store and Subtyping
(pdf)
Jan Schwinghammer
Italian Conference on Theoretical Computer Science (ICTCS'05)
A Concurrent Lambda Calculus with Futures
(pdf)
Joachim Niehren, Jan Schwinghammer, Gert Smolka
5th International Workshop on Frontiers in Combining Systems
Efficiently Computing the Density of Regular Languages
Manuel Bodirsky, Tobias Gärtner, Timo vonOertzen, Jan Schwinghammer
LATIN 2004: Theoretical Informatics: 6th Latin American Symposium
A Concurrent Lambda-Calculus with Promises and Futures
(pdf)
Jan Schwinghammer
Master's Thesis, Programming Systems Lab, Universität des Saarlandes