Bernardo Toninho

E-mail: b ++ toninho ++ @fct.unl.pt or b ++ toninho ++ @gmail.com

Room: 239 (Dep. Informatica, FCT NOVA)

Phone: Office - (+351) 21 294 85 36, Ext. 10766

  

  

I am an assistant professor (Professor Auxiliar) in Departamento de Informática at Faculdade de Ciências e Tecnologia (Universidade NOVA de Lisboa). I am also a member of NOVA-LINCS.

In my previous life I was a postdoc with Nobuko Yoshida's Mobility Reading Group at Imperial College London. In my other previous life, I did my PhD at Carnegie Mellon University and Universidade Nova de Lisboa with Frank Pfenning and Luís Caires.


Research

I am interested in the application of language-based techniques to the development of more robust and safer concurrent and distributed systems. More specifically, I work within the realm of (substructural) type theory, such as those based on Linear Logic and Session Types, and their applications to concurrent programming. I am also interested in using type and logic-based techniques to verify concurrent programs in real languages such as Go, Rust and Scala.

I am a strong advocate of computational trinitarianism and in finding out what it has to say about concurrency.

Links to my DBLP, Google Scholar, ORCID and GitHub profiles.

Teaching

2018/19, 1st Semester: Introduction to Programming

2017/18, 2nd Semester: Analysis and Design of Algorithms (in Portuguese)


Assorted Drafts

B. Toninho. Categories for Linear Logic. (Text Draft)

Publications and Talks

S. Balzer, F. Pfenning, B. Toninho
A Universal Session Type for Untyped Asynchronous Communication.
To Appear at International Conference on Concurrency Theory (CONCUR 2018) (Full version pdf)

B. Toninho
Depending on Session-Typed Processes.
Special session on Session Types
Mathematical Foundations of Programming Semantics (MFPS 2018) (Talk)

B. Toninho, N. Yoshida
Depending on Session-Typed Processes.
Foundations of Software Science and Computation Structures (FoSSaCS 2018) (Open Access DOI)

B. Toninho, N. Yoshida
On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings.
European Symposium on Programming (ESOP 2018) (Open Access DOI)

J. Lange, N. Ng, B. Toninho, N. Yoshida
A Static Verification Framework for Message Passing in Go using Behavioural Types.
International Conference on Software Engineering (ICSE 2018) (Open Access DOI)

J. Lange, N. Ng, B. Toninho, N. Yoshida
Liveness and Safety for Channel-based Programming in Go.
Principles of Programming Languages (2017) (Errata) (Long Version) (DOI) (Tool)

L. Caires, F. Pfenning, B. Toninho
Linear Logic Propositions as Session Types.
Mathematical Structures in Computer Science (2016) (DOI)

B. Toninho, N. Yoshida
Certifying Data in Multiparty Session Types.
A List of Successes That Can Change the World (Wadlerfest - 2016) (DOI)

M. Bartoletti, I. Castellani, P.-M. Deniélou, M. Dezani-Ciancaglini, S. Ghilezane, J. Pantovice, J. Pérez, P. Thiemann, B. Toninho, H. T. Vieira.
Combining Behavioural Types with Security Analysis.
Journal of Logical and Algebraic Methods in Programming (2015) (DOI) (ArXiv)

B. Toninho. PhD Thesis: A Logical Foundation for Session-based Concurrent Computation.
(Document) (Slides)

B. Toninho. Thesis Proposal: A Logical Foundation for Session-based Concurrent Computation.
(Document) (Slides)

B. Toninho, L. Caires, F. Pfenning. Corecursion and Non-Divergence in Session Types.
Trustworthy Global Computing 2014 (TGC'14). (Full Version pdf)

B. Toninho, L. Caires, F. Pfenning. Higher-Order Processes, Functions, and Sessions: A Monadic Integration.
European Symposium on Programming (ESOP'13). (Full Version pdf)

L. Caires, J. Pérez, F. Pfenning, B. Toninho. Behavioral Polymorphism and Parametricity in Session-Based Communication.
European Symposium on Programming (ESOP'13). (Full Version pdf)

B. Toninho. Linear Logic: A Logical Foundation for Concurrent Computation.
Curry-Howard: Logic and Computation Monthly Meeting (CHoCoLa, Lyon, Oct. 12) - Invited Talk (Slides)

H. DeYoung, L. Caires, F. Pfenning, B. Toninho. Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication.
Computer Science Logic (CSL'12). (Full Version pdf)

R. Simmons, B. Toninho. Constructive Provability Logic.
Submitted (Draft)

L. Caires, F. Pfenning, B. Toninho. Linear Logic Propositions as Session Types.
Submitted (Updated Draft)

B. Toninho, L. Caires, F. Pfenning. Functions as Session-Typed Processes.
Foundations of Software Science and Computation Structures (FoSSaCS'12). (Full Version pdf)

J. Pérez, L. Caires, F. Pfenning, B. Toninho. Linear Logical Relations for Session-Based Concurrency.
European Symposium on Programming (ESOP'12) (Full Version pdf)

L. Caires, F. Pfenning, B. Toninho. Towards Concurrent Type Theory .
Types in Language Design and Implementation (TLDI'12) - Invited Talk. (Full Version pdf)

F. Pfenning, L. Caires, B. Toninho. Proof-Carrying Code in a Session-Typed Process Calculus.
Certified Programs and Proofs (CPP'11). (Full Version pdf)

B. Toninho, L. Caires, F. Pfenning. Dependent Session Types via Intuitionistic Linear Type Theory.
Principles and Practice of Declarative Programming (PPDP'11) (Full Version pdf)

R. Simmons, B. Toninho. Constructive Provability Logic.
Intuitionistic Modal Logics and Applications Workshop (IMLA'11) (Full Version pdf)

R. Simmons, B. Toninho, F. Pfenning. Distributed deductive databases, declaratively.
The L10 logic programming language.
ACM SIGPLAN X10 Workshop 2011 (Full Version pdf)

B. Toninho, L. Caires. A Spatial-Epistemic Logic for Reasoning about Security Protocols.
8th International Workshop on Security Issues in Concurrency (SecCo'10), Paris 2010. (Full Version pdf)

B. Toninho. A Logic and Tool for Local Reasoning about Security Protocols.
MSc Dissertation (2009). (Full Version pdf)

Technical Reports

L. Caires, J. Pérez, F. Pfenning, B. Toninho. Relational Parametricity for Polymorphic Session Types.
CMU Technical Report CMU-CS-12-108 (Full Version pdf)

B. Toninho, L. Caires, F. Pfenning. Dependent Session Types via Intuitionistic Linear Type Theory.
CMU Technical Report CMU-CS-11-139. (Full Version pdf)

L. Caires, F. Pfenning, B. Toninho. Session Types as Intuitionistic Linear Propositions.
CMU Technical Report CMU-CS-11-138. (Full Version pdf)

R. Simmons, B. Toninho. Principles of Constructive Provability Logic.
CMU Technical Report CMU-CS-10-151. (Full Version pdf)

B. Toninho, L. Caires. A Spatial-Epistemic Logic and Tool for Reasoning about Security Protocols.
Tech. Report, DI-FCT-UNL (2009). (Full Version pdf)

Assorted Projects, Talks and Stuff

US Physical Keyboard with PT Layout Driver (includes working < and >).
All Archs. (Installer)

B. Toninho. A Logical Foundation for Proof-Carrying Communicating Processes.
Speaking Skills Talk (Joint work with Luis Caires and Frank Pfenning). (Slides)

R. Simmons, B. Toninho. Logic Programming in Constructive Provability Logic.
Modal Logic 15-816 Class Project (2010). (Full Version pdf)

F. Militão, K. Naden, B. Toninho. Improving RRT with Context Sensitivity.
Grad. Artificial Intelligence 15-780 Class Project (2010). (Full Version pdf)

K. Naden, B. Toninho. Improving Local Processing of Network Data with NIC on-chip Caching.
Grad. Computer Networks 15-744 Class Project (2010). (Full Version pdf)