Publications

Quick Links


Journal Articles

  1. Featherweight Go
    Robert Griesemer, Raymond Hu, Wen Kokke, Julien Lange, Ian Taylor, Bernardo Toninho, Philip Wadler, and Nobuko Yoshida
    Proc. of the ACM on Programming Languages (PACMPL) issue ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH-OOPSLA), vol. 3, 2020
    [PDF, Code, Talk]
  2. Refinement kinds: Type-safe Programming with Practical Type-level Computation
    Luís Caires and Bernardo Toninho
    Proc. of the ACM on Programming Languages (PACMPL) issue ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH-OOPSLA), vol. 3, 2019
    [PDF, Code, Talk]
  3. Interconnectability of Session-Based Logical Processes
    Bernardo Toninho and Nobuko Yoshida
    ACM Trans. on Programming Languages and Systems (TOPLAS), vol. 40, num. 4, 2018, 1:1–1:42
    [PDF, Talk]
  4. Certifying data in multiparty session types
    Bernardo Toninho and Nobuko Yoshida
    Journal of Logic and Algebraic Methods in Programming (JLAMP), vol. 90, 2017
    [PDF]
  5. Linear logic propositions as session types
    Luís Caires, Frank Pfenning, and Bernardo Toninho
    Mathematical Structures in Computer Science (MSCS), 2016
    [PDF]
  6. Combining behavioural types with security analysis
    Massimo Bartoletti, Ilaria Castellani, Pierre-Malo Deniélou, Mariangola Dezani-Ciancaglini, Silvia Ghilezan, Jovanka Pantovic, Jorge A. Pérez, Peter Thiemann, Bernardo Toninho, and Hugo Torres Vieira
    Journal of Logic and Algebraic Methods in Programming (JLAMP), vol. 84, num. 6, 2015
    [PDF]
  7. Linear logical relations and observational equivalences for session-based concurrency
    Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho
    Information and Computation (I&C), vol. 239, 2014
    [PDF]

Peer-Reviewed Book Chapters

  1. Polymorphic Session Processes as Morphisms
    Bernardo Toninho and Nobuko Yoshida
    The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy - Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday (Palamidessifest), 2019
    [PDF]
  2. Certifying Data in Multiparty Session Types
    Bernardo Toninho and Nobuko Yoshida
    A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (Wadlerfest), 2016
    [PDF]

Peer-Reviewed Conference and Workshop Papers

  1. Domain-Aware Session Types
    Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho
    Int. Conf. on Concurrency Theory (CONCUR), 2019
    [PDF]
  2. Manifest Deadlock-Freedom for Shared Session Types
    Stephanie Balzer, Bernardo Toninho, and Frank Pfenning
    Programming Languages and Systems - European Symposium on Programming (ESOP), 2019
    [PDF]
  3. A Universal Session Type for Untyped Asynchronous Communication
    Stephanie Balzer, Frank Pfenning, and Bernardo Toninho
    Int. Conf. on Concurrency Theory (CONCUR), 2018
    [PDF]
  4. On Polymorphic Sessions and Functions - A Tale of Two (Fully Abstract) Encodings
    Bernardo Toninho and Nobuko Yoshida
    Programming Languages and Systems - European Symposium on Programming (ESOP), 2018
    [PDF]
  5. Depending on Session-Typed Processes
    Bernardo Toninho and Nobuko Yoshida
    Int. Conf. on Foundations of Software Science and Computation Structures (FoSSaCS), 2018
    [PDF]
  6. A Static Verification Framework for Message Passing in Go using Behavioural Types
    Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida
    ACM and IEEE Int. Conf. on Software Engineering (ICSE), 2018
    [PDF]
  7. Fencing off go: liveness and safety for channel-based programming
    Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida
    ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017
    [PDF, Code]
  8. Corecursion and Non-divergence in Session-Typed Processes
    Bernardo Toninho, Luís Caires, and Frank Pfenning
    Trustworthy Global Computing (TGC), 2014
    [PDF]
  9. Behavioral Polymorphism and Parametricity in Session-Based Communication
    Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho
    Programming Languages and Systems - European Symposium on Programming (ESOP), 2013
    [PDF]
  10. Higher-Order Processes, Functions, and Sessions: A Monadic Integration
    Bernardo Toninho, Luís Caires, and Frank Pfenning
    Programming Languages and Systems - European Symposium on Programming (ESOP), 2013
    [PDF]
  11. Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication
    Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho
    Annual Conf. of the EACSL, Computer Science Logic (CSL), 2012
    [PDF]
  12. Linear Logical Relations for Session-Based Concurrency
    Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho
    Programming Languages and Systems - European Symposium on Programming (ESOP), 2012
    [PDF]
  13. Functions as Session-Typed Processes
    Bernardo Toninho, Luís Caires, and Frank Pfenning
    Int. Conf. on Foundations of Software Science and Computation Structures (FoSSaCS), 2012
    [PDF]
  14. Towards concurrent type theory
    Luís Caires, Frank Pfenning, and Bernardo Toninho
    ACM SIGPLAN Int. Workshop on Types in Languages Design and Implementation (TLDI), 2012
    [PDF]
  15. Proof-Carrying Code in a Session-Typed Process Calculus
    Frank Pfenning, Luís Caires, and Bernardo Toninho
    ACM SIGPLAN Int. Conf. on Certified Programs and Proofs (CPP), 2011
    [PDF]
  16. Dependent session types via intuitionistic linear type theory
    Bernardo Toninho, Luís Caires, and Frank Pfenning
    ACM SIGPLAN Int. Symp. on Principles and Practice of Declarative Programming (PPDP), 2011
    [PDF]
  17. Constructive Provability Logic
    Robert J. Simmons and Bernardo Toninho
    Int. Workshop on Intuitionistic Modal Logics and Applications (IMLA), 2011
    [PDF]
  18. Distributed deductive databases, declaratively: The L10 logic programming language
    Robert J. Simmons, Bernardo Toninho, and Frank Pfenning
    ACM SIGPLAN X10 Workshop (X10), 2011
    [PDF]
  19. A Spatial-Epistemic Logic for Reasoning about Security Protocols
    Bernardo Toninho and Luís Caires
    Int. Workshop. on Security Issues in Concurrency (SecCo), 2010
    [PDF]

Invited Talks

  1. Linear Logic: A Logical Foundation for Concurrent Computation
    Bernardo Toninho
    Curry-Howard: Logic and Computation Monthly Meeting (Lyon), 2012
    [PDF]
  2. Session Types and Linear Logic
    Bernardo Toninho
    University of Bath, 2017
    [PDF]
  3. Depending on Session-typed Processes
    Bernardo Toninho
    Mathematical Foundations of Programming Semantics, 2018
    [Abstract, PDF]

    Session types are a typing discipline for message-passing concurrency that enables the specification of communication protocols as channel types, which can then be statically and/or dynamically enforced in order to ensure various correctness properties such as deadlock-freedom and protocol compliance.

    However, in most session typing frameworks the language of types (and so, the language of protocols) is kept fairly limited, consisting mainly of sequential descriptions of input and output actions, combined with some form of branching or alternative behaviours.

    In this talk I will present a dependent type theory, realised in a concurrent functional language based on the Curry-Howard interpretation of linear logic, that allows for session processes to depend on functions and vice-versa, as well as for the definition of type-level functions. By enriching the type language in this way, we are able to specify protocols where the choice of the next communication action can truly depend on the specific values of exchanged data – a significant gain in expressiveness wrt the state of the art. I will also show how the type theoretic nature of the framework allows us to internally describe and prove predicates on process behaviours, akin to dependently-typed specifications of functional programs.

    Finally, in order to both justify some of our design choices and to benchmark the expressiveness of the theory I will introduce a faithful embedding (up-to the theory’s internal equality) of the functional layer of the calculus within the session-typed process layer.

  4. Session Types, Linear Logic and Lightweight Applications of Session Types in Java
    Bernardo Toninho and Raymond Hu
    University College London, 2017
    [PDF]
  5. Refinement Kinds
    Bernardo Toninho
    Facebook London, 2019
    [PDF]
  6. Refinement Kinds
    Bernardo Toninho
    Faculty of Science, University of Lisbon, 2019
    [PDF]
  7. Featherweight Go
    Raymond Hu, Julien Lange, and Bernardo Toninho
    Go London User Group, 2021
    [Talk]

Theses and Other Papers

  1. A Logical Foundation for Session-based Concurrent Computation
    Bernardo Toninho
    PhD thesis, Carnegie Mellon University and NOVA University of Lisbon, 2015
    [PDF]
  2. A Logic and Tool for Local Reasoning about Security Protocols
    Bernardo Toninho
    MSc thesis, School of Science and Technology, NOVA University of Lisbon, 2009
    [PDF, Code]