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 and Talks

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)

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)

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)

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, 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)