 |
|
|
| @N.A. Charlton, B. Horsfall, B. Reus: Crowfoot: A Verifier for Higher-Order Store Programs.
VMCAI 2012, LNCS 7148, pp. 136-151.
|
| |
| B. Reus, Th. Streicher: Relative Completeness for Logics of Functional Programs. CSL 2011, pp.470-480.
| | |
| @ J. Schwinghammer, L. Birkedal, B. Reus, H. Yang: Nested Hoare Triples and Frame Rules for Higher-order Store, Logical Methods in Computer Science 7(3): (2011).
|
| |
| @ N.A. Charlton, B. Reus: Specification Patterns and Proofs for Recursion through the Store, FCT 2011, LNCS 6914, pp 310-321.
| |
| |
| @ N.A. Charlton, B. Horsfall, B. Reus: Formal Reasoning about Runtime Code Update, HotSWUp 2011 (Hot Topics in Software Upgrades), ICDE Workshops 2011: 134-138.
|
| |
| @ L. Birkedal, B. Reus, J. Schwinghammer, Kristian
Stovring, Jacob Thamsborg, and H. Yang: Step-Indexed Kripke Models over Recursive Worlds,
POPL 2011, January 2011. ACM pp.119-132. |
| |
| @ N. Charlton,
B. Reus: A deeper
understanding of the deep frame axiom (extended abstract), 9 pages, presented at Workshop
LoLA'10, Edinburgh.
|
| |
| @ J. Schwinghammer, H. Yang,
L. Birkedal, F. Pottier,
A semantic foundation for hidden state,
Fossacs, LNCS 6014, pp.2-17, 2010. |
| |
| @ N. Charlton, B. Reus: A decidable class of verification conditions for programs with higher order store,
AVOCS 09, Electronic
Communications of the Association of Software Science and Technology (EASST) 23, 2010. Also in University of Swansea,
Technical Report CSR-2-2009. |
| |
| @ J. Schwinghammer, L. Birkedal, B. Reus, H. Yang: Nested Hoare Triples and Frame Rules for Higher-Order Store,
CSL 09, LNCS 5771, pp.440-454, 2009. |
| |
| @ L.Birkedal, B.Reus, J.Schwinghammer, H.Yang: A Simple Model of Separation Logic for Higher-order Store,
ICALP (II), LNCS 5126, pp. 348-360, 2008. |
| |
| @ B.Reus, J. Schwinghammer: Separation Logic for Higher-Order
Store,
CSL '06, LNCS 4207, pp. 575-590, Springer-Verlag, Berlin,
2006. |
| |
| @ B.Reus, J. Schwinghammer: Denotational Semantics for Program
Logic of Objects MSCS, vol.16:313-358. Cambridge
University, 2006. |
| |
| @ D. Pattinson, B.Reus : A Complete Temporal And Spatial Logic For Distributed Systems. FroCos 05, LNAI 3717,
pp.122-137, Springer Berlin, 2005. |
| |
| @ B.Reus, Th. Streicher: About Hoare Logic for Higher-Order Store. ICALP 05, LNCS 3580,
pp.1337-1348, 2005. |
| |
| @ B.Reus, J. Schwinghammer: Denotational Semantics for Abadi and Leino's Logic of Objects. ETAPS 05, LNCS 3444,
pp. 263-178, Springer Berlin, 2005. |
| |
| @ B.Reus, Th. Streicher: Semantics and logics of object calculi. TCS(316):191-213, 2004. |
| |
| @ B.Reus: Modular Semantics and Logics of Classes. CSL'03.
LNCS 2803, pp.456-469, Springer Verlag, Berlin, 2003. |
| |
| @ B. Reus: Class-based versus Object-based: A Denotational Comparison. AMAST '02. LNCS 2422, pp. 473-488, Springer Verlag, Berlin, 2002. |
| |
| @ B. Reus, Th. Streicher: Semantics and Logics of Objects. LICS '02, Copenhagen. (version 24/09/02 including some corrections). IEEE Press 2002. |
| |
| @ U. Berger, K-H. Niggl, B. Reus (guest editors) Theoretical Computer Science Vol. 264(2), Workshop On Domains III (Selected Papers), 2001. |
| |
| @ B. Reus, M. Wirsing, R. Hennicker: A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Model. FASE'01, ETAPS, Genova, LNCS 2029, pp. 300-316, Springer Berlin, 2001. |
| |
| @ B. Reus, T. Hein: Towards a Machine-Checked Java Specification Book.
Theorem Proving in Higher Order Logics:
TPHOLs 2000,
LNCS 1869, p.479-496, Springer Berlin 2000. |
| |
| @ Th. Altenkirch, B. Reus: Monadic presentations
of lambda terms using generalized inductive types.
CSL'99. LNCS Springer Berlin, 1999. |
| |
| @ Th. Altenkirch, W. Naraschewski, B. Reus (Eds.): Types for Proofs
and Programs. Proceedings of the Types Working Group Meeting at Kloster
Irsee, 1998. LNCS 1657, Springer, Berlin, 1999. |
| |
| @ B. Reus: Formalizing a variant of Synthetic Domain Theory.
Journ. of Automated Reasoning 23:411-444, 1999. |
| |
| @ P. Cenciarelli, A. Knapp, B. Reus, M. Wirsing : An Event-Based Structual Operational Semantcis of Multi-Threaded Java: , In Jim Alves-Foss (Ed.) Formal Syntax and Semantics Of Java, LNCS 1523, pp. 157-200, Springer, Berlin, 1999. |
| |
| @ B. Reus: Extensional Sigma-Spaces in Type Theory. Journal of Applied Categorical Structures 7:159-183, Kluwer Academic Publishers, 1999. |
| |
| @ B. Reus, T. Streicher: General Synthetic Domain Theory - A Logical Approach. MSCS 9:177--223. Cambridge University Press, 1999. |
| |
| @ T. Streicher, B. Reus: Classical logic: Continuation Semantics and Abstract Machines. Journal of Functional Programming. Vol 8(6), pp. 543-572, 1998. This is the original extended version also containing cbv, not the Journal version |
| |
| @ P. Cenciarelli, A. Knapp, B. Reus, M. Wirsing : From Sequential To Multi-Threaded Java:
An Event-Based Operational Semantics, AMAST'97, LNCS 1349, pp. 402-417, Springer Berlin, 1997. |
| |
| @ B. Reus, A. Knapp, P. Cenciarelli, M. Wirsing : Verifying a Compiler Optimization for Multi-Threaded Java, WADT Workshop 97, LNCS 1376, Springer, Berlin, 1998 |
| |
| @ U. Berger, K.-H. Niggl, B. Reus (eds.): Workshop Domains III (Proceedings), Technical Report 9712, Ludwig-Maximilians-Universität, München, 1997. |
| |
| @ B. Reus, T. Streicher : General Synthetic Domain Theory -- A Logical Approach (extended abstract), CTCS'97, Santa Margherita, Italy. LNCS 1290, pp. 293-313, Springer, Berlin, 1997.
|
| |
| @ B. Reus : Synthetic Domain Theory in Type Theory : Another Logic of Computable Functions, TPHOL 96, Turku, 1996, LNCS 1125, Springer Verlag, 1996. |
| |
| @ B. Reus : Program Verification in Synthetic Domain Theory. Thesis, November 1995.
Shaker Verlag Aachen, 1996. |
| |
| @ Y. Lafont, B. Reus, T. Streicher: Continuations Semantics or Expressing Implication by Negation. Technical Report 9321, Ludwig-Maximilians-Universität, München, 1993.
Since there have been some requests for this here is a PS version.
|
| |
| @ B. Reus,T. Streicher: Naive Synthetic Domain Theory - A Logical Approach. Unpublished internal report, Universität München, 1993. It is the precursor of the MSCS journal paper. |
| |
| @ B. Reus, T. Streicher: Verifying Properties of Module Construction in Type Theory. In A.M. Borzyszkowski, S. Sokolowski (eds.)
MFCS'93, Springer Verlag, Lecture Notes in Computer Science 711, Berlin, September 1993.
See also Lifting the laws of module algebra to deliverables. Technical Report 9203, Ludwig-Maximilians-Universität, München, August 1992. |
|
Bernhard's Papers
