Bernardo Toninho

e-mail: first_letter_of_first_name ++ last_name@gmail.com or @cs.cmu.edu

FCT-UNL Office: 314

CMU Office: GHC 9005

  

Graduated BSc (1º Ciclo) in Computer Science at FCT-UNL in 2007.

Graduated MSc (2º Ciclo) in Computer Science at FCT-UNL in 2009.

Currently, I am a Computer Science PhD student at CMU and FCT-UNL, co-advised by Frank Pfenning and Luís Caires.

Research Interests

My research interests focus on the development and application of logic and formal languages in Computer Science.

Mainly, my interests lie in modal logic, type theory, programming languages and calculi (with a focus on concurrency, distribution and security).

Publications

L. Caires, J. Pérez, F. Pfenning, B. Toninho. Relational Parametricity for Polymorphic Session Types.
Submitted (Draft) (Extended Version)

H. DeYoung, L. Caires, F. Pfenning, B. Toninho. Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication.
Submitted (Draft)

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

L. Caires, F. Pfenning, B. Toninho. Linear Logic Propositions as Session Types.
Submitted (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)

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)

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)

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 for Reasoning about Security Protocols.
8th International Workshop on Security Issues in Concurrency (SecCo'10), Paris 2010. (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)

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

Assorted Projects and Talks

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)