The research was led by Luís Caires, CMU Portugal Scientific Director and Faculty member at Nova Lincs/ FCT-UNL and Frank Pfenning, CMU School of Computer Science, as a key component of Bernardo Toninho’s Dual Degree Ph.D. in Computer Science, supervised by both faculty. Toninho joined the CMU Portugal Program in the end of 2009 as a dual PhD student and graduated in 2015. His Ph.D. research was focused on the logical foundations of message-passing concurrent computation, based on a so-called propositions-as-types correspondence between logic and programming languages.
The paper “Dependent session types via intuitionistic linear type theory” was published in the ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming (PPDP) in 2011 and will be presented at this year’s conference in September. This award is given each year to a paper from the PPDP proceedings published 10 years earlier and is intended to “recognize the authors’ contribution to PPDP’s influence in the area of declarative programming.” The winning work introduced a novel notion of so-called dependent session types, a highly expressive specification and verification mechanism for message-passing concurrent programs, able to check for functional and communication correctness properties of programs without running them.
More about the INTERFACES project
The “INTERFACES project – Certified Interfaces for Integrity and Security in Extensible Web-based Applications” was carried out between 2009 and 2012 by teams from Universidade Nova de Lisboa (UNL), Faculdade de Ciências da Universidade de Lisboa (FCUL), Carnegie Mellon University and the Company, OutSystems
The project targeted the development of new techniques and tools for enforcing security, integrity, and correctness requirements on distributed extensible web-based applications by introducing novel, semantically rich notions of interface description languages, based on advanced type systems and logics.
Key outputs of the INTERFACES approach included core typed programming languages and environments for building extensible certified web applications, as well as design and implementations of prototypes for specification, programming, and reasoning about case studies, in collaboration with the industrial partner OutSystems SA, developer of the Agile Platform, a widely used web-based application development environment at the time.
Original article at Nova Lincs website.