Selected Publications

2025

• Loyal, L., Jürchott, K., Reimer, U., Meyer-Arndt, L., Henze, L., Mages, N., . . . Thiel, A. (2025). Aging and Viral Evolution Impair Immunity Against Dominant Pan-Coronavirus-Reactive T Cell Epitope. European Journal of Immunology, 55(7). doi:10.1002/eji.202551888
  Article. View online.

2024

• Loyal, L., Jürchott, K., Reimer, U., Meyer-Arndt, L., Henze, L., Mages, N., . . . Thiel, A. (2024). Aging and viral evolution impair immunity against dominant pan-coronavirus-reactive T cell epitope. doi:10.1101/2024.08.21.608923
  Preprint. View online.

2023

• Fuhrmann, S., Reus, B., Frey, O., Pera, A., Picker, L., & Kern, F. (2023). Marked skewing of entire T-cell memory compartment occurs only in a minority of CMVinfected individuals and is unrelated to the degree of memory subset skewing among CMVspecific T-cells. Frontiers in Immunology, 14, pages. doi:10.3389/fimmu.2023.1258339
  Article. View on figshare.
• Knapp, A., Mühlberger, H., & Reus, B. (2023). Interpreting knowledge-based programs. In ESOP 2023 : 32st European Symposium on Programming Vol. 13990 (pp. pages). Paris, France: Springer. doi:10.1007/978-3-031-30044-8_10
  Conference publication. View on figshare.
• Knapp, A., Mühlberger, H., & Reus, B. (2023). Interpreting Knowledge-based Programs (Extended Version with Proofs). doi:10.48550/arxiv.2301.10807
  Preprint. View online.

2021

• Reus, B., Caserta, S., Larsen, M., Morrow, G., Bano, A., Hallensleben, M., . . . Kern, F. (2021). In-depth profiling of T-cell responsiveness to commonly recognized CMV antigens in older people reveals important sex differences. Frontiers in Immunology, 12, 1-21. doi:10.3389/fimmu.2021.707830
  Article. View on figshare.
• Kirkham, F., Pera, A., Simanek, A. M., Bano, A., Morrow, G., Reus, B., . . . Kern, F. (2021). Cytomegalovirus infection is associated with an increase in aortic stiffness in older men which may be mediated in part by CD4 memory T-cells. Theranostics, pages. doi:10.7150/thno.58356
  Article. View on figshare.

2020

• Klimis, V., Parisis, G., & Reus, B. (2020). Model checking software-defined networks with flow entries that time out. In Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design – FMCAD 2020 Vol. 1 (pp. 179-184). Wien: IEEE. doi:10.34727/2020/isbn.978-3-85448-042-6_25
  Conference publication. View on figshare.
• Klimis, V., Parisis, G., & Reus, B. (2020). Model Checking Software-Defined Networks with Flow Entries that Time Out (version with appendix). Retrieved from http://arxiv.org/abs/2008.06149v2
  Preprint.
• Klimis, V., Parisis, G., & Reus, B. (2020). Towards model checking real-world software-defined networks. In Computer Aided Verification. CAV 2020. Lecture Notes in Computer Science Vol. 12225 (pp. 126-148). Los Angeles, California, USA: Springer Verlag. doi:10.1007/978-3-030-53291-8_8
  Conference publication. View on figshare.
• Klimis, V., Parisis, G., & Reus, B. (2020). Towards Model Checking Real-World Software-Defined Networks (version with appendix). Retrieved from http://arxiv.org/abs/2004.11988v5
  Preprint.

2018

• Rojas, A. P., Caserta, S., Albanese, F., Blowers, P., Morrow, G., Terrazzini, N., . . . Kern, F. (2018). CD28null pro-atherogenic CD4 T-cells explain the link between CMV infection and an increased risk of Cardiovascular death. Theranostics, 8(16), 4509-4519. doi:10.7150/thno.27428
  Article. View on figshare.

2017

• Altenkirch, T., Capriotti, P., & Reus, B. (2017). Domain theory in type theory via QIITs. In Leibniz International Proceedings in Informatics Lipics Vol. 104 (pp. 16-17).
  Conference publication.

2016

• Reus, B. (2016). Limits of Computation. Springer International Publishing. doi:10.1007/978-3-319-27889-6
  Book. View online.

2015

• Reus, B., Charlton, N., & Horsfall, B. (2015). Symbolic execution proofs for higher order store programs. Journal of Automated Reasoning, 54(3), 199-284. doi:10.1007/s10817-014-9319-8
  Article. View on figshare.

2013

• Charlton, N., & Reus, B. (2013). Specification patterns for reasoning about recursion through the store. Information and Computation, 231, 167-203. doi:10.1016/j.ic.2013.08.011
  Article. View on figshare.

2012

• Schwinghammer, J., Birkedal, L., Pottier, F., Reus, B., Stovring, K., & Yang, H. (2012). A step-indexed Kripke model of hidden state. Mathematical Structures in Computer Science, 23(1), 1-54. doi:10.1017/S0960129512000035
  Article. View on figshare.
• Horsfall, B., Charlton, N., & Reus, B. (2012). Verifying the reflective visitor pattern. In Proceedings for Ftfjp 2012 the 14th Workshop on Formal Techniques for Java Like Programs Co Located with Ecoop 2012 and PLDI 2012 Papers Presented at the Workshop (pp. 27-34). doi:10.1145/2318202.2318208
  Conference publication. View online.
• Reus, B., & Streicher, T. (2012). A synthetic theory of sequential domains. Annals of Pure and Applied Logic, 163(8), 1062-1074. doi:10.1016/j.apal.2011.12.028
  Article. View online.
• Charlton, N., Horsfall, B., & Reus, B. (2012). Crowfoot: a verifier for higher-order store programs. In Verification, Model Checking, and Abstract Interpretation (Vol. 7148, pp. 136-151). Springer. doi:10.1007/978-3-642-27940-9_10
  Chapter. View on figshare.

2011

• Schwinghammer, J., Birkedal, L., Reus, B., & Yang, H. (2011). Nested Hoare Triples and Frame Rules for Higher-order Store. Logical Methods in Computer Science, 7(3), 1-42. doi:10.2168/LMCS-7(3:21)2011
  Article. View on figshare.
• Schwinghammer, J., Birkedal, L., Reus, B., & Yang, H. (2011). Nested Hoare Triples and Frame Rules for Higher-order Store. doi:10.48550/arxiv.1109.3031
  Preprint. View online.
• Reus, B., & Streicher, T. (2011). Relative Completeness for Logics of Functional Programs. In Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011. Bergen (Norway).
  Presentation. View on figshare.
• Charlton, N., & Reus, B. (2011). Specification patterns and proofs for recursion through the store. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 6914 LNCS (pp. 310-321). doi:10.1007/978-3-642-22953-4_27
  Conference publication. View online.
• Charlton, N., Horsfall, B., & Reus, B. (2011). Formal reasoning about runtime code update. In Proceedings International Conference on Data Engineering (pp. 134-138). doi:10.1109/ICDEW.2011.5767624
  Conference publication. View online.
• Birkedal, L., Reus, B., Schwinghammer, J., Støvring, K., Thamsborg, J., & Yang, H. (2011). Step-indexed kripke models over recursive worlds. In ACM SIGPLAN Notices Vol. 46 (pp. 119-131). doi:10.1145/1925844.1926401
  Conference publication. View online.
• Birkedal, L., Reus, B., Schwinghammer, J., Stovring, K., Thamsborg, J., & Yang, H. (2011). Step-indexed kripke models over recursive worlds. In POPL '11 Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Vol. 38, pp. 119-132). ACM.
  Chapter. View on figshare.

2010

• Reus, B., Jung, A., Keimel, K., & Streicher, T. (2010). Preface for the special issue on domains. Mathematical Structures in Computer Science, 20(2), 105-106. doi:10.1017/S0960129509990338
  Article. View online.
• Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F., & Reus, B. (2010). A semantic foundation for hidden state. In FOSSACS 2010. Paphos.
  Presentation. View on figshare.

2009

• Schwinghammer, J., Birkedal, L., Reus, B., & Yang, H. (2009). Nested hoare triples and frame rules for higher-order store. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 5771 LNCS (pp. 440-454). doi:10.1007/978-3-642-04027-6_32
  Conference publication. View online.
• Charlton, N., & Reus, B. (2009). A decidable class of verification conditions for programs with higher order store. In Electronic Communications of the Easst Vol. 23. doi:10.14279/tuj.eceasst.23.318.303
  Conference publication. View online.

2008

• Birkedal, L., Reus, B., Schwinghammer, J., & Yang, H. (2008). A simple model of separation logic for higher-order store. In 35th International Colloquium on Automata, Languages and Programming. Keykjavik, ICELAND, JUL 07-11, 2008. doi:10.1007/978-3-540-70583-3_29
  Presentation. View on figshare.

2007

• Reus, B. (1996). Synthetic domain theory in type theory: Another logic of computable functions. In Theorem Proving in Higher Order Logics (Vol. 1125, pp. 363-380). Springer Nature. doi:10.1007/bfb0105416
  Chapter. View online.

2006

• Reus, B., & Schwinghammer, J. (2006). Separation Logic for Higher-Order Store. In Computer Science Logic 2006. Szeged, Hungary.
  Presentation. View on figshare.
• Reus, B., & Schwinghammer, J. (2006). Denotational semantics for a program logic of objects. Mathematical Structures in Computer Science, 16(2), :313-358. doi:10.1017/S0960129506005214
  Article. View on figshare.

2005

• Reus, B., & Streicher, T. (2005). About Hoare logics for higher-order store. In 32nd International Colloquium on Automata, Languages and Programming Languages (ICALP), LNCS. Lisbon. doi:10.1007/11523468
  Presentation. View on figshare.
• Reus, B., & Schwinghammer, J. (2005). Denotational semantics for Abadi and Leino's logic of objects. In Unknown Book (Vol. 3444, pp. 16.0 pages). Springer.
  Chapter. View on figshare.
• Pattinson, D., & Reus, B. (2005). A complete temporal and spatial logic for distributed dystems. In Frontiers of Combining Systems: Proceedings of the 5th International Workshop, FroCoS 2005, Vienna, Austria (Vol. 3717, pp. 122-137). Springer. doi:10.1007/11559306_7
  Chapter. View on figshare.
• Reus, B., & Streicher, T. (2005). About Hoare logics for higher-order store. In Automata, Languages and Programming: Proceedings of the 32nd International Colloquim, ICALP 2005, Lisbon, Portugal (Vol. 3580, pp. 1337-1348). Berlin, Germany: Springer Verlag. doi:10.1007/11523468_108
  Chapter. View on figshare.
• Reus, B., & Schwinghammer, J. (2005). Denotational Semantics for Abadi and Leino’s Logic of Objects. doi:10.1007/978-3-540-31987-0_19
  Presentation. View online.
• Reus, B., & Schwinghammer, J. (2005). Denotational semantics for Abadi and Leino's logic of objects. In Programming Languages and Systems: Proceedings of the 14th European Symposium on Programming, ESOP 2005, Edinburgh, UK (Vol. 3444, pp. 263-278). Springer. doi:10.1007/b107380
  Chapter. View on figshare.

2004

• Reus, B., & Streicher, T. (2004). Semantics and logic of object calculi. Theoretical Computer Science, 316(1-3), 191-213. doi:10.1016/j.tcs.2004.01.030
  Article. View on figshare.

2003

• Reus, B. (2003). Modular semantics and logics of classes. In 12th Annual Conference of the European-Association-for-Computer-Logic/8th Kurt Godel Colloquium/17th International Workshop on Computer Science Logic. Vienna, Austria. doi:10.1007/b13224
  Presentation. View on figshare.
• Altenkirch, T., & Reus, B. (1999). Monadic Presentations of Lambda Terms Using Generalized Inductive Types. In Lecture Notes in Computer Science (pp. 453-468). Springer Berlin Heidelberg. doi:10.1007/3-540-48168-0_32
  Chapter. View online.
• Reus, B. (2003). Modular Semantics and Logics of Classes. In Lecture Notes in Computer Science (pp. 456-469). Springer Berlin Heidelberg. doi:10.1007/978-3-540-45220-1_37
  Chapter. View online.
• Reus, B. (2003). Modular semantics and logics of classes. In Unknown Book (Vol. 2803, pp. 456-469). doi:10.1007/978-3-540-45220-1_37
  Chapter. View online.

2002

• Reus, B., & Streicher, T. (2002). Semantics and logic of object calculi. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (pp. 113-122). IEEE Publications. doi:10.1109/LICS.2002.1029821
  Chapter. View on figshare.
• Cenciarelli, P., Knapp, A., Reus, B., & Wirsing, M. (1999). An Event-Based Structural Operational Semantics of Multi-threaded Java. In Lecture Notes in Computer Science (pp. 157-200). Springer Berlin Heidelberg. doi:10.1007/3-540-48737-9_5
  Chapter. View online.
• Reus, B. (2002). Class-based versus object-based: A denotational comparison. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 2422 (pp. 473-488). doi:10.1007/3-540-45719-4_32
  Conference publication. View online.
• Reus, B. (2002). Class-based versus object-based: a denotational comparison. In Algebraic Methodology and Software Technology: Proceedings of the 9th International Conference, AMAST 2002, Saint-Gilles-les- Bains, Reunion Island, France (Vol. 2422, pp. 45-88). London, UK.: Springer-Verlag. doi:10.1007/3-540-45719-4
  Chapter. View on figshare.

2001

• Reus, B., Wirsing, M., & Hennicker, R. (2001). A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Models. In Lecture Notes in Computer Science (pp. 300-317). Springer Berlin Heidelberg. doi:10.1007/3-540-45314-8_22
  Chapter. View online.
• Berger, U., Niggl, K. H., & Reus, B. (2001). Theoretical computer science: Preface. Theoretical Computer Science, 264(2), 169. doi:10.1016/S0304-3975(00)00220-6
  Article. View online.
• Reus, B., Wirsing, M., & Hennicker, R. (2001). A hoare calculus for verifying java realizations of OCL-constrained design models. In Unknown Book (Vol. 2029, pp. 300-317). doi:10.1007/3-540-45314-8_22
  Chapter. View online.
• Reus, B., Wirsing, M., & Hennicker, R. (2001). A Hoare calculus for verifying Java realizations of OCL-constrained design models. In Proceedings in Fundamental Approaches to Software Engineering: 4th International Conference, FASE 2001, Genova, Italy (Vol. 2029, pp. 300-317). Springer Berlin / Heidelberg. doi:10.1007/3-540-45314-8
  Chapter. View on figshare.

2000

• Reus, B., & Hein, T. (2000). Towards a machine-checked java specification book. In Unknown Book (Vol. 1869, pp. 480-497). doi:10.1007/3-540-44659-1_30
  Chapter. View online.
• Reus, B., & Hein, T. (2000). Towards a Machine-Checked Java Specification Book. In Lecture Notes in Computer Science (pp. 480-497). Springer Berlin Heidelberg. doi:10.1007/3-540-44659-1_30
  Chapter. View online.
• Reus, B., & Hein, T. (2000). Towards a machine-checked Java specification book. In Theorem Proving in Higher Order Logics: Proceedings of the 13th International Conference, TPHOLs 2000 Portland, OR, USA (Vol. 1869, pp. 480-497). Springer-Verlag. doi:10.1007/3-540-44659-1
  Chapter. View on figshare.

1999

• Reus, B. (1999). Realizability models for type theories. In Electronic Notes in Theoretical Computer Science Vol. 23 (pp. 128-158). doi:10.1016/S1571-0661(04)00108-2
  Conference publication. View online.
• Reus, B. (1999). Formalizing synthetic domain theory - the basic definitions. Journal of Automated Reasoning, 23(3-4), 411-444. doi:10.1023/A:1006258506401
  Article. View on figshare.
• Reus, B. (1999). Extensional S-spaces in type theory. Applied Categorical Structures, 7(1-2), 159-183.
  Article. View on figshare.
• Cenciarelli, P., Knapp, A., Reus, B., & Wirsing, M. (1999). An event-based structural operational semantics of multi-threaded java. In Unknown Book (Vol. 1523, pp. 157-200). doi:10.1007/3-540-48737-9_5
  Chapter. View online.
• Reus, B. (1999). Extensional Σ-Spaces in Type Theory. Applied Categorical Structures, 7(1-2), 159-183. doi:10.1023/a:1008600521659
  Article. View online.
• Altenkirch, T., & Reus, B. (1999). Monadic presentations of lambda terms using generalized inductive types. In Unknown Book (Vol. 1683, pp. 453-468). doi:10.1007/3-540-48168-0_32
  Chapter. View online.
• Reus, B., & Streicher, T. (1999). General Synthetic Domain Theory - A Logical Approach.. Mathematical Structures in Computer Science, 9(2), 177-223. doi:10.1017/S096012959900273X
  Article. View on figshare.
• Altenkirch, T., & Reus, B. (1999). Monadic presentations of Lambda terms using generalized inductive types. In Computer Science Logic: Proceedings of the 13th International Workshop CSL '99, 8th Annual Conference of the EACSL, Madrid, Spain (Vol. 1863, pp. 453-468). Springer-Verlag. doi:10.1007/3-540-48168-0
  Chapter. View on figshare.
• Cenciarelli, P., Knapp, A., Reus, B., & Wirsing, M. (1999). An event-based structural operational semantics of multi-threaded Java. In Formal Syntax and Semantics of Java (Vol. 1523, pp. 157-200). Berlin, Germany: Springer-Verlag. doi:10.1007/3-540-48737-9
  Chapter. View on figshare.

1998

• Reus, B., Knapp, A., Cenciarelli, P., & Wirsing, M. (1998). Verifying a compiler optimization for multi-threaded java. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 1376 (pp. 402-417). doi:10.1007/3-540-64299-4_47
  Conference publication. View online.
• Streicher, T., & Reus, B. (1998). Classical logic, continuation semantics and abstract machines. Journal of Functional Programming, 8(6), 543-572. doi:10.1017/S0956796898003141
  Article. View on figshare.

1997

• Cenciarelli, P., Knapp, A., Reus, B., & Wirsing, M. (1997). From sequential to multi-threaded java: An event-based operational semantics. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 1349 (pp. 75-90). doi:10.1007/bfb0000464
  Conference publication. View online.
• Reus, B., & Streicher, T. (1997). General synthetic domain theory — a logical approach. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 1290 (pp. 293-313). doi:10.1007/bfb0026995
  Conference publication. View online.

1996

• Reus, B. (1996). Synthetic domain theory in type theory: Another logic of computable functions. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 1125 (pp. 365-380). doi:10.1007/bfb0105416
  Conference publication. View online.

1993

• Reus, B., & Streicher, T. (1993). Verifying properties of module construction in type theory. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 711 LNCS (pp. 660-670). doi:10.1007/3-540-57182-5_57
  Conference publication. View online.

1992

• Reus, B. (1992). Implementing higher-order functions in an algebraic specification language with narrowing. In Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics Vol. 631 LNCS (pp. 483-484). doi:10.1007/3-540-55844-6_160
  Conference publication. View online.