Books

• B. Jacobs, Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, North Holland, Elsevier, 1999.
  Please contact Elsevier or Amazon for information on how to order this book
• B. Jacobs, Introduction to Coalgebra. Towards Mathematics of States and Observations. Two-thirds of a book in preparation; comments are welcome.
• B. Jacobs, De Menselijke Maat in ICT, 2007. Free online book, in Dutch.

Papers

2007

• J.-H. Hoepman, B. Jacobs, Increased security through open source, Communications of the ACM 50(1), 2007. p.79-83.
  [DOI link]
  

Opinion articles/columns

• B. Jacobs, W. Teepe, Raar dat stemhulp alles van u weet in: Volkskrant, 5/03/07.
  As a result of this article the national privacy commissioner (College Bescherming Persoonsgegevens) has decided to start an investigation into the privacy management of the voting advice site Stemwijzer, see for instance this news flash.

2006

• B. Jacobs, S. Smetsers, R. Wichers Schreur, Code-carrying theories, Formal Aspects of Computing, 2006.
  [DOI link]
  
• B. Jacobs and I. Hasuo, Semantics and Logic for Security Protocols.
  [ copy] [ accompanying PVS sources]
  
• J.-H. Hoepman, E. Hubbers, B. Jacobs, M. Oostdijk, and R. Wichers Schreur. Crossing Borders: Security and Privacy Issues of the European e-Passport. In 1st Int. Workshop on Security, Kyoto, Japan, October 23-24 2006. Springer LNCS 4266, p.152-167.
  [DOI link] [copy]
  
• B. Jacobs, A Bialgebraic Review of Deterministic Automata, Regular Expressions and Languages. In: K. Futatsugi, J.-P. Jouannaud, J. Meseguer (Eds.), Algebra, Meaning and Computation: Essays dedicated to Joseph A. Goguen on the Occasion of his 65th Birthday. Springer LNCS 4060, p.375--404, 2006. © Springer-Verlag
  [DOI link] [Earlier Technical report ICIS-R05003]
• B. Jacobs and I. Hasuo, Freyd is Kleisli, for Arrows. In: eWiC proceedings of: Workshop on Mathematically Structured Functional Programming (MSFP'06).
  [copy]
  
• B. Jacobs, Distributive laws for the Coinductive Solution of Recursive Equations, Information and Computation 204(4), 2006, p.561-587.
  [DOI link] [local copy]
  
• C. Heunen and B. Jacobs, Arrows, like Monads, are Monoids. To appear in the ENTCS proceedings of MFPS 22.
  [copy]
  
• I. Hasuo, B. Jacobs and A. Sokolova, Generic Trace Theory. To appear in the ENTCS proceedings of CMCS 2006.
  [copy]
  
• B. Jacobs, J. Rusby, PVS. In: F. Wiedijk, The Seventeen Provers of the World, Springer LNAI 3600, p.24--27, 2006.

Opinion articles/columns

• Spoken column from a discussion evening in political and cultural centre De Balie, Amsterdam 17 nov. 2006.
• B. Jacobs, Stemcomputer vraagt om fraude in national newspaper NRC Handelsblad (and also in the companion paper NRC.next), 12/10/06.
• B. Jacobs, Biometrische gegevens horen niet in Databank in: Volkskrant, 28/02/06.
• J.-H. Hoepman and B. Jacobs, E-passports without the big picture, on: egovmonitor.com, 20/02/06.
• B. Jacobs, Burger moet geen gelabeld vee worden, in: Reformatorisch Dagblad, 17/02/06.

2005

• B. Jacobs, Select before you Collect Ars Aequi, jaargang 54, dec. 2005, p.1006-1009 (in Dutch).
  [copy]
  
• E. Hubbers, B. Jacobs, and W. Pieters. RIES - Internet Voting in Action. In: R. Bilof (ed.), Proceedings of the 29th Annual International Computer Software and Applications Conference, COMPSAC'05, p.417-424. IEEE Computer Society, 2005.
  [copy]
  
• C.-B. Breunesse, B. Jacobs, N. Cataño and M. Huisman, Formal Methods for Smart Cards: an experience report. Science of Computer Programming 55 (2005), p.53-80.
  [DOI link]
  
• I. Hasuo, B. Jacobs, Context-free Languages via Coalgebraic Trace Semantics. In: J.L. Fiadeiro, N. Harman, M. Roggenbach, J. Rutten (Eds.), Algebra and Coalgebra in Computer Science (CALCO'05) Springer LNCS 3629, p.213--231, 2005. © Springer-Verlag
  [DOI link] [Technical report ICIS-R05004 ]
• B. Jacobs, W. Pieters and M. Warnier, Statically checking confidentiality via dynamic labels. In the proceedings of the Workshop on Issues in the Theory of Security (WITS'05)
  [copy]

2004

• E. Hubbers, B. Jacobs, W. Pieters, RIES - Internet Voting in Action. Technical Report NIII-R0449, Institute for Computing and Information Sciences, University of Nijmegen.
  [copy]
• B. Jacobs, `Vakmanschap van overwegend belang binnen informatiebeveiliging', Questafette in the magazine Informatiebeveiliging, nr. 6, 2004, p.4-5.
• B. Jacobs, E. Poll, Java Program Verification at Nijmegen: Developments and Perspective. In: K. Futatsugi and F. Mizoguchi and N. Yonezaki (Eds.), Software Security -- Theories and Systems (ISSS'03) Springer LNCS 3233, p.134--153, 2004. © Springer-Verlag
  [DOI link] [Technical report NIII 3018]
• E. Hubbers, B. Jacobs, Stemmen via internet geen probleem, Automatisering Gids on 15 okt. 2004.
  [copy]
  
• J. Hughes and B. Jacobs, Simulations in Coalgebra. Theoretical Computer Science, 327(1-2) p.71-108, 2004
  [DOI link]
  
• B. Jacobs, Ongebreidelde functionaliteit grootste vijand beveiliging, Automatisering Gids on 24 sept. 2004.
  [copy]
  
• B. Jacobs, C. Marche and N. Rauch, Formal verification of a commercial smart card applet with multiple tools. In: C. Rattray and S. Maharaj and C. Shankland (Eds.), Algebraic Methodology and Software Technology (AMAST'04), Springer LNCS 3116, p.21--22 2004. © Springer-Verlag
  [DOI link]
  
• E. Hubbers, B. Jacobs, J. Kiniry, M. Oostdijk, Counting votes with formal methods. In: C. Rattray and S. Maharaj and C. Shankland (Eds.), Algebraic Methodology and Software Technology (AMAST'04), Springer LNCS 3116, p.241-257 2004. © Springer-Verlag
  [DOI link] [local copy]
  [The Java + JML open source files of the ``KOA'' project mentioned in this abstract are available via OSOSS]
  
• B. Jacobs, Frits Vaandrager, Onderzoeksagenda remt innovatief onderzoek. Automatisering Gids on 9 July 2004.
  [copy]
  
• B. Jacobs, Relating two Approaches to Coinductive Solution of Recurisve Equations. In: J. Adámek and S. Milius (eds), Coalgebraic Methods in Computer Science (CMCS) 2004, Electr. Notes in Theor. Comp. Sci. 106, 2004.
  [copy] [DOI link]
  
• B. Jacobs, Trace Semantics for Coalgebras, In: J. Adámek and S. Milius (eds), Coalgebraic Methods in Computer Science (CMCS) 2004, Electr. Notes in Theor. Comp. Sci. 106, 2004.
  [copy] [DOI link]
  
• B. Jacobs, Weakest Precondition Reasoning for Java Programs with JML Annotations. Journal of Logic and Algebraic Programming 58, p.61-88.
  [DOI link]
  
• B. Jacobs, M. Oostdijk, M. Warnier, Source Code Verification of a Secure Payment Applet, Journal of Logic and Algebraic Programming, 58 p.107-120.
  [DOI link]
  

2003

• B. Jacobs, J. Kiniry, M. Warnier, Java Program Verification Challenges. In: F. de Boer, M. Bonsangue, S. Graf, W.-P. de Roever (Eds.), Formal Methods for Components and Objects (FMCO 2002) Springer LNCS 2852, p.202-219, 2003. © Springer-Verlag
  Technical Report NIII-R0310, Institute for Computing and Information Sciences, University of Nijmegen.
  [DOI link] [copy]
• J.-H. Hoepman and B. Jacobs, Open source software. Bron van vertrouwen, I&I;, 21(6), 2003 p.12-19.
  [copy]
• J.-H. Hoepman and B. Jacobs, Elektronisch handtekening. Wie tekent ervoor?, I&I;, 21(3), 2003, p.8-9.
  [copy]
  See also the resulting Editorial comment (hoofdartikel, © NRC) in the national newspaper NRC of sept. 2, 2003.
• B. Jacobs Informatici moeten meer optreden in de media. In: Automatisering Gids on 23 may 2003
  [copy] [picture © Automatisering Gids]
• B. Jacobs, De Computer de Wet Gesteld, Inaugural Speech, 16 may 2003, ISBN 90 901 6917 2.
  [copy]
• B. Jacobs, Java's Integral Types in PVS. In: E. Najim, U. Nestmann, P. Stevens (Eds.), Formal Methods for Open Object-Based Distributed Systems (FMOODS 2003) Springer LNCS 2884, p.1-15, 2003. © Springer-Verlag
  [DOI link] [copy]
• B. Jacobs and E. Poll, Coalgebras and monads in the semantics of Java. Theoretical Computer Science, 291/3 p.329-349, 2003.
  [DOI link]
  

2002

• B. Jacobs, The temporal logic of coalgebras via Galois algebras Mathematical Structure in Computer Science 12, p.875-903, 2002.
  [Reprint available on request.]
  Technical Report CSI-R9906, Computing Science Institute, University of Nijmegen.
  [copy]
• C.-B. Breunesse, B. Jacobs and J. van den Berg, Specifying and verifying a decimal representation in Java for Smart Cards. In: H. Kirchner and C. Ringeissen (Eds.), Algebraic Methodology and Software Technology (AMAST'02), Springer LNCS 2422, p.304-318, 2002. © Springer-Verlag
  [copy]
• J. Hughes and B. Jacobs, Factorization systems and fibrations: Toward a fibred Birkhoff variety theorem, Electr. Notes in Theor. Comp. Sci. 69, 2002. (Special issue on the conference of CTCS 2002)
  [copy] [DOI link]
• B. Jacobs, Comprehension for Coalgebras Electr. Notes in Theor. Comp. Sci. 65-1, 2002. (Special issue on the workshop Coalgebraic Methods in Computer Science (CMCS 2002))
  [copy] [DOI link]
• B. Jacobs, Exercises in Coalgebraic Specification In: R. Backhouse, R. Crole and J. Gibbons (eds.) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction (Springer LNCS 2297, 2002), p.237-280. © Springer-Verlag
  (Manuscript for the proceedings of the Mathematics for Information Technology summer school, Oxford, 10-14 April 2000.)
  [postscript copy] [pdf copy]

2001

• B. Jacobs, JavaCard Program Verification In: R.J. Boulton and P.B. Jackson (eds.), Theorem Proving in Higher Order Logics (TPHOLs 2001), (Springer LNCS 2152, 2001), p.1-3. © Springer-Verlag
  [copy]
  
• J. van den Berg, B. Jacobs, E. Poll, Formal Specification and Verification of JavaCard's Application Identifier Class In: I. Attali and Th. Jensen (eds.), Java on Smart Cards: Programming and Security (Springer LNCS 2041, 2001) p.137-150. © Springer-Verlag Proceedings of the Java Card 2000 Workshop
  [copy]
• B. Jacobs, H. Meijer and E. Poll, VerifiCard: A European Project for Smart Card Verification. In: Newsletter 5 of the Dutch Association for Theoretical Computer Science (NVTI), 2001
  [copy]
• B. Jacobs, Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study Theoret. Informatics and Applications 35(1) (2001) p.31-59.
  [Reprint available on request.]
  [copy of technical report]
  
• J. van den Berg, B. Jacobs, The LOOP compiler for Java and JML In: T. Margaria and W. Yi (eds.), Tools and Algorithms for the Construction and Analysis of Software (TACAS), (Springer LNCS 2031, 2001) 299--312. © Springer-Verlag
  [copy]
  
• B. Jacobs, E. Poll A Logic for the Java Modeling Language JML In: H. Hussmann (ed.), Fundamental Approaches to Software Engineering (FASE), (Springer LNCS 2029, 2001), p.284-299. © Springer-Verlag
  [copy]
  
• E. Poll, J. van den Berg, B. Jacobs, Formal Specification of the JavaCard API in JML: the APDU class. Computer Networks 36(4) (2001) p.407-421.
  [copy of technical report]
• B. Jacobs, A Formalisation of Java's Exception Mechanism In: D. Sands (ed.), Programming Languages and Systems (ESOP), (Springer LNCS 2028, 2001), p.284-301. © Springer-Verlag
  [copy]
  
• J. Rothe, B. Jacobs, H. Tews, The Coalgebraic Class Specification Language CCSL. Journal of Universal Computer Science, 7(2), 2001.
  [copy]
  
• M. Huisman, B. Jacobs, J. van den Berg, A case study in class library verification: Java's vector class. Software Tools for Technology Transfer 3(3), 2001, p.332-352.
  Available as Technical Report CSI-R0007, Computing Science Institute, University of Nijmegen.
  [copy]
  
• E. Poll, J. van den Berg, B. Jacobs, Formal Specification of the JavaCard API in JML: the APDU class Computer Networks 36(4), 2001, p.407-421.
  (An earlier version is available as Techn. Rep. CSI-R0005, Computing Science Institute, Univ. Nijmegen, 2000.)
  [copy]

2000

• G.T. Leavens, K.R.M. Leino, E. Poll, C. Ruby, and B. Jacobs. JML: notations and tools supporting detailed design in Java. To appear in OOPSLA 2000 Companion, Minneapolis, Minnesota. Copyright ACM, 2000. Also Department of Computer Science, Iowa State University, TR #00-15, August 2000
  [copy]
  
• B. Jacobs, Object-oriented hybrid systems of coalgebras plus monoid actions. Theor. Comput. Science 239 (2000), p.41-95.
  [Reprint available on request.]
  
• M. Huisman, B. Jacobs, Inheritance in Higher Order Logic: Modeling and Reasoning. In: M. Aagaard and J. Harrison (eds.) Theorem Proving in Higher Order Logics (TPHOL) Springer LNCS 1869, p.301-319, 2000. © Springer-Verlag
  [copy]
  
• E. Poll, J. van den Berg, B. Jacobs, Specification of the JavaCard API in JML In: J. Domingo-Ferrer and D. Chan and A. Watson (eds.), Smart Card Research and Advanced Application (IFIP Cardis 2000) (Kluwer Acad. Publ. 2000), p.135--154
  [copy]
• B. Jacobs, Towards a Duality Result in the Modal Logic of Coalgebras. Electr. Notes in Theor. Comp. Sci. 33, 2000. (Special issue on the workshop Coalgebraic Methods in Computer Science (CMCS 2000))
  [copy]
• B. Jacobs, E. Poll, A Monad for Basic Java Semantics. In: T. Rus (ed), Algebraic Methodology and Software Technology (AMAST'00), Springer LNCS 1816, p.150-164, 2000. © Springer-Verlag
  [copy]
  (An earlier version is available as Techn. Rep. CSI-R9926, Computing Science Institute, Univ. Nijmegen, 1999.)
• J. van den Berg, M. Huisman, B. Jacobs, E. Poll, A Type-Theoretic Memory Model for Verification of Sequential Java Programs. In: In D. Bert, C. Choppy, and P.D. Mosses (eds.), Recent Trends in Algebraic Development Techniques, Springer LNCS 1827, 2000, p.1-21. © Springer-Verlag
  [copy]
  
• M. Huisman, B. Jacobs, Java Program Verification via a Hoare Logic with Abrupt Termination. In: T. Maibaum (ed), Fundamental Approaches to Software Engineering (FASE'00), Springer LNCS 1783, p.284-303, 2000. © Springer-Verlag
  [copy]
  (An earlier version is available as Techn. Rep. CSI-R9912, Computing Science Institute, Univ. Nijmegen, 1999.)

1999

• B. Jacobs, Coalgebras in Specification and Verification for Object-Oriented Languages. In: Newsletter 3 of the Dutch Association for Theoretical Computer Science (NVTI), 1999, p.15-27.
  [copy]
• U. Hensel and B. Jacobs, Coalgebraic Theories of Sequences in PVS.
  Journal of Logic and Computation 9(4), 1999, p.463-500.
  [postscript copy] [pdf copy]
  The paper describes a fully formalised and verified coalgebraic theory of sequences in the prototype verification system PVS. The PVS sources are available.
• B. Jacobs, Abstracte Programmeerkunst, Over de grenzen van het weten. Jaarboek 1999, Vereniging van Akademie-onderzoekers.

1998

• B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, H. Tews, Reasoning about Java Classes (Preliminary Report). Object-Oriented Programming Systems, Languages and Applications, ACM Press, p.329-340, 1998.
  [copy]
  
• U. Hensel, M. Huisman, B. Jacobs, H. Tews, Reasoning about Classes in Object-Oriented Languages: Logical Models and Tools. In: Ch. Hankin (ed), European Symposium on Programming, LNCS 1381, p.105-121, 1998. © Springer-Verlag
  [copy]
  (An earlier version is available as Technical Report CSI-R9718, Computing Science Institute, University of Nijmegen.)
• B. Jacobs, Coalgebraic Reasoning about Classes in Object-Oriented Languages. Electr. Notes in Theor. Comp. Sci. 11, 1998. (Special issue on the workshop Coalgebraic Methods in Computer Science (CMCS 1998))
  [copy] [DOI link]
• C. Hermida and B. Jacobs, Structural induction and coinduction in a fibrational setting, Information and Computation 145 (1998), p.107-152.
  [Reprint available on request.]

1997

• B. Jacobs and J. Rutten, A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin 62, 1997, p.222-259.
  [postscript copy] [pdf copy]
• B. Jacobs, Invariants, Bisimulations and the Correctness of Coalgebraic Refinements. In: M. Johnson (ed), Algebraic Methodology and Software Technology, LNCS 1349, p.276-291, 1997. © Springer-Verlag
  [copy]
• U. Hensel and B. Jacobs, Proof Principles for Iterated Datatypes. In: E. Moggi and G. Rosolini (eds), Category Theory and Computer Science, LNCS 1290, p.220-241, 1997. © Springer-Verlag
  [copy]
• B. Jacobs, Behaviour-Refinement of Coalgebraic Specifications with Coinductive Correctness Proofs. In: M. Bidoit and M. Dauchet (eds.) TAPSOFT'97: Theory and Practice of Software Development Springer LNCS 1214, p.787-802, 1997.
  [copy]

1996

• B. Jacobs, Coalgebraic specifications and models of deterministic hybrid systems. In: M. Wirsing and M. Nivat (eds.) Algebraic Methodology and Software Technology (AMAST), Springer LNCS 1101, 1996, p.520-535.
  [copy] (july 1996)
• B. Jacobs, Inheritance and cofree constructions. In: P. Cointe (ed.) European Conference on object-oriented programming (ECOOP) (Springer LNCS 1098, Berlin, 1996) 210 - 231.
  [copy]
• B. Jacobs, Objects and classes, co-algebraically. In: B. Freitag, C.B. Jones, C. Lengauer, and H.-J. Schek (eds) Object-Orientation with Parallelism and Persistence Kluwer Acad. Publ., 1996, p. 83--103.
  [copy]
• B. Jacobs, On Cubism. Journ. of Functional Programming 6, p.379-391, 1996.
  [copy]

1995

• B. Jacobs, Mongruences and cofree coalgebras. In: V.S. Alagar and M. Nivat (eds.) Algebraic Methodology and Software Technology (AMAST 1995) Springer LNCS 936, 1995, p.245-260.
  [copy]
• C. Hermida and B. Jacobs, Fibrations with indeterminates: Contextual and Functional Completeness for Polymorphic Lambda Calculi. Math. Struct. in Comp. Sci. 5 (4) (1995), 501 - 531.
  [Reprint available on request.]

1994

• C. Hermida and B. Jacobs, An algebraic view of structural induction. In: L. Pacholski and J. Tiuryn (eds.) Proceedings Computer Science Logic 1994 (Springer LNCS 933, Berlin 1995), 412 - 426.
  [copy]
  
• M. Bonsangue, B. Jacobs and J. Kok, Duality beyond Sober Spaces: Topological Spaces and Observation Frames Theor. Comp. Sci. 151 (1) (1995), 79 - 124.
• B. Jacobs, Parameters and Parametrization in Specification, using distributive categories. Fundamenta Informaticae 24 (3) (1995), 209 - 250.
  [copy]
• B. Jacobs, Subtypes and bounded quantification from a fibred perspective Electr. Notes in Theor. Comp. Sci. 1 (Proceedings of Mathematical Foundations of Program Semantics, New Orleans, April 1995.)
  [copy] [DOI link]
• B. Jacobs, Coalgebras and Approximation. In: A. Nerode and Yu. V. Matiyasevich (eds.) Logical Foundations of Computer Science, St. Petersburg, (Springer LNCS 813, Berlin 1994), 173 - 183.
  [copy]
• B. Jacobs, Semantics of Weakening and Contraction. Annals of Pure and Applied Logic 69 (1994), 73 - 106.

1993

• B. Jacobs and T. Melham, Translating Dependent Type Theory into Higher Order Logic. In: M. Bezem and J.F. Groote (eds.) Typed Lambda Calculi and Applications, Utrecht, (Springer LNCS 664, Berlin, 1993), 209 - 229.
• B. Jacobs, Semantics of Lambda-I and of other ``substructure'' Lambda Calculi. In: M. Bezem and J.F. Groote (eds.) Typed Lambda Calculi and Applications, Utrecht, (Springer LNCS 664, Berlin, 1993), 195-208.
  [copy]
• B. Jacobs, Comprehension Categories and the Semantics of Type Dependency. Theor. Comp. Sci. 107 (1993), 169 - 207.

1992

• B. Jacobs, Simply Typed and Untyped Lambda Calculus Revisited. In: M.P. Fourman, P.T. Johnstone and A.M. Pitts (eds.) Applications of Category Theory in Computer Science (LMS 177, Camb. Univ. Press, 1992), 119 - 142.
  [copy]
• B. Jacobs, I. Margaria and M. Zacchi Filter lambda models with Polymorphic Types. Theor. Comp. Sci. 95 (1) (1992), 143 - 158.

1991

• B. Jacobs, Semantics of the second order Lambda Calculus. Math. Struct. in Comp. Sci. 1 (1991), 327 - 360.
• B. Jacobs, Categorical Type Theory PhD. Thesis, University of Nijmegen, 1991.
  [copy]
• B. Jacobs, E. Moggi and Th. Streicher Relating Models of impredicative Type Theories. In: D.H. Pitt et al., (eds.), Category Theory and Computer Science (Springer LNCS 530, Berlin, 1991), 197 - 218.

1989

• B. Jacobs, On the Semantics of second order Polymorphic Lambda Calculus: form Bruce-Meyer-Mitchell models to Hyperdoctrine models and vice-versa. In: D.H. Pitt et al., (eds.), Category Theory and Computer Science (Springer LNCS 389, Berlin, 1989), 198 - 212.
• B. Jacobs, The Inconsistency of Higher Order Extensions of Martin-Lof's Type Theory. Journ. Phil. Log. 18 (1989), 399 - 422.