Implementing Higher-Order Functions in an Algebraic Specification Language with Narrowing. - Bernhard Reus (PLILP, 1992)

Verifying Properties of Module Construction in Type Theory. - Bernhard Reus; Thomas Streicher (MFCS, 1993)

Synthetic Domain Theory in Type Theory: Another Logic of Computable Functions. - Bernhard Reus (TPHOLs, 1996)

Program verification in synthetic domain theory. - Bernhard Reus (Shaker, 1996)

From Sequential to Multi-Threaded Java: An Event-Based Operational Semantics. - Pietro Cenciarelli; Alexander Knapp; Bernhard Reus; Martin Wirsing (AMAST, 1997)

Verifying a compiler optimization for Multi-Threaded Java. - Bernhard Reus; Alexander Knapp; Pietro Cenciarelli; Martin Wirsing (WADT, 1997)

Classical Logic, Continuation Semantics and Abstract Machines. - Thomas Streicher; Bernhard Reus (J. Funct. Program., 1998)

Monadic Presentations of Lambda Terms Using Generalized Inductive Types. - Thorsten Altenkirch; Bernhard Reus (CSL, 1999)

A Logic of Recursive Objects. - Bernhard Reus (ECOOP Workshops, 1999)

An Event-Based Structural Operational Semantics of Multi-Threaded Java. - Pietro Cenciarelli; Alexander Knapp; Bernhard Reus; Martin Wirsing (Formal Syntax and Semantics of Java, 1999)

Extensional Sigma-Spaces in Type Theory. - Bernhard Reus (Appl. Categorical Struct., 1999)

Realizability Models for Type Theories. - Bernhard Reus (Realizability Semantics and Applications@FLoC, 1999)

Formalizing Synthetic Domain Theory. - Bernhard Reus (J. Autom. Reason., 1999)

General synthetic domain theory - a logical approach. - Bernhard Reus; Thomas Streicher (Math. Struct. Comput. Sci., 1999)

Towards a Machine-Checked Java Specification Book. - Bernhard Reus; Tatjana Hein (TPHOLs, 2000)

A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Models. - Bernhard Reus; Martin Wirsing; Rolf Hennicker (FASE, 2001)

Preface. - Ulrich Berger 001; Karl-Heinz Niggl; Bernhard Reus (Theor. Comput. Sci., 2001)

Class-Based versus Object-Based: A Denotational Comparison. - Bernhard Reus (AMAST, 2002)

Modular Semantics and Logics of Classes. - Bernhard Reus (CSL, 2003)

Semantics and logic of object calculi. - Bernhard Reus; Thomas Streicher (Theor. Comput. Sci., 2004)

Denotational Semantics for Abadi and Leino's Logic of Objects. - Bernhard Reus; Jan Schwinghammer (ESOP, 2005)

A Complete Temporal and Spatial Logic for Distributed Systems. - Dirk Pattinson; Bernhard Reus (FroCoS, 2005)

About Hoare Logics for Higher-Order Store. - Bernhard Reus; Thomas Streicher (ICALP, 2005)

Separation Logic for Higher-Order Store. - Bernhard Reus; Jan Schwinghammer (CSL, 2006)

Denotational semantics for a program logic of objects. - Bernhard Reus; Jan Schwinghammer (Math. Struct. Comput. Sci., 2006)

A Simple Model of Separation Logic for Higher-Order Store. - Lars Birkedal; Bernhard Reus; Jan Schwinghammer; Hongseok Yang (ICALP (2), 2008)

A decidable class of verification conditions for programs with higher order store. - Nathaniel Charlton; Bernhard Reus (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2009)

A Semantic Foundation for Hidden State. - Jan Schwinghammer; Hongseok Yang; Lars Birkedal; François Pottier; Bernhard Reus (FoSSaCS, 2010)

Preface for the special issue on domains. - Bernhard Reus; Achim Jung; Klaus Keimel; Thomas Streicher (Math. Struct. Comput. Sci., 2010)

Relative Completeness for Logics of Functional Programs. - Bernhard Reus; Thomas Streicher (CSL, 2011)

Specification Patterns and Proofs for Recursion through the Store. - Nathaniel Charlton; Bernhard Reus (FCT, 2011)

Formal reasoning about runtime code update. - Nathaniel Charlton; Ben Horsfall; Bernhard Reus (ICDE Workshops, 2011)

Step-indexed kripke models over recursive worlds. - Lars Birkedal; Bernhard Reus; Jan Schwinghammer; Kristian Støvring; Jacob Thamsborg; Hongseok Yang (POPL, 2011)

Nested Hoare Triples and Frame Rules for Higher-order Store - Jan Schwinghammer; Lars Birkedal; Bernhard Reus; Hongseok Yang (Log. Methods Comput. Sci., 2011)

Verifying the reflective visitor pattern. - Ben Horsfall; Nathaniel Charlton; Bernhard Reus (FTfJP@ECOOP, 2012)

Crowfoot: A Verifier for Higher-Order Store Programs. - Nathaniel Charlton; Ben Horsfall; Bernhard Reus (VMCAI, 2012)

A synthetic theory of sequential domains. - Bernhard Reus; Thomas Streicher (Ann. Pure Appl. Log., 2012)

Specification patterns for reasoning about recursion through the store. - Nathaniel Charlton; Bernhard Reus (Inf. Comput., 2013)

A step-indexed Kripke model of hidden state. - Jan Schwinghammer; Lars Birkedal; François Pottier; Bernhard Reus; Kristian Støvring; Hongseok Yang (Math. Struct. Comput. Sci., 2013)

Symbolic Execution Proofs for Higher Order Store Programs. - Bernhard Reus; Nathaniel Charlton; Ben Horsfall (J. Autom. Reason., 2015)

Limits of Computation - From a Programming Perspective - Bernhard Reus (Springer, 2016)

Towards Model Checking Real-World Software-Defined Networks. - Vasileios Klimis; George Parisis; Bernhard Reus (CAV (2), 2020)

Model Checking Software-Defined Networks with Flow Entries that Time Out. - Vasileios Klimis; George Parisis; Bernhard Reus (FMCAD, 2020)

Interpreting Knowledge-based Programs. - Alexander Knapp; Heribert Mühlberger; Bernhard Reus (ESOP, 2023)

Interpreting Knowledge-based Programs (Extended Version with Proofs). - Alexander Knapp; Heribert Mühlberger; Bernhard Reus (CoRR, 2023)