AVÊÓƵ

Selected Publications

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. .

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. .
• 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. .
• Knapp, A., Mühlberger, H., & Reus, B. (2023). Interpreting Knowledge-based Programs (Extended Version with Proofs). doi:10.48550/arxiv.2301.10807
  Preprint. .

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. .
• Kirkham, F., Pera, A., Simanek, A. M., Bano, A., Morrow, G., Reus, B., . . . Kern, F. (n.d.). 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. .

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. .
• 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, July 19). 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. .
• 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. .

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. .

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. .

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. .

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. .
• 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. .
• 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. .
• 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. .

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. .
• 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. .
• 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. .
• 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. .
• 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. .
• 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. .
• 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. .

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. .
• Schwinghammer, J., Yang, H., Birkedal, L., Pottier, F., & Reus, B. (2010). A semantic foundation for hidden state. In FOSSACS 2010. Paphos.
  Presentation. .

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. .
• 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. .

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. .

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. .

2006

• Reus, B., & Schwinghammer, J. (2006). Separation Logic for Higher-Order Store. In Computer Science Logic 2006. Szeged, Hungary.
  Presentation. .
• 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. .

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. .
• 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. .
• 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. .
• 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. .
• 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. .
• 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. .

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. .

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. .
• 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. .
• 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. .
• 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. .

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. .
• 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. .
• 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. .
• 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. .

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. .
• 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. .
• 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. .
• 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. .

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. .
• 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. .
• 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. .

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. .
• 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. .
• Reus, B. (1999). Extensional S-spaces in type theory. Applied Categorical Structures, 7(1-2), 159-183.
  Article. .
• 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. .
• Reus, B. (1999). Extensional Σ-Spaces in Type Theory. Applied Categorical Structures, 7(1-2), 159-183. doi:10.1023/a:1008600521659
  Article. .
• 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. .
• 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. .
• 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. .
• 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. .

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. .
• 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. .

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. .
• 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. .

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. .

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. .

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. .