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