RSS Meetups are monthly gatherings of LASIGE members with interests in Software Architecture, Verification, Testing, Programming Languages, Type Systems, Logic, Concurrency, Formal methods and other topics.

Title: Refinement Kinds

Speaker: Bernardo Toninho (FCT-UNL)

When: Friday, December 6th, 15h30

Where: C6.3.27

Abstract:

In this talk I will introduce the concept of kind refinement, which we develop in the context of an explicitly polymorphic ML-like language with type-level computation. Just as type refinements embed rich specifications by means of comprehension principles expressed by predicates over values in the type domain, kind refinements provide rich kind specifications by means of predicates over types in the kind domain. By leveraging our powerful refinement kind discipline, types in our language are not just used to statically classify program expressions and values, but also conveniently manipulated as tree-like data structures, with their kinds refined by logical constraints on such structures. Remarkably, the resulting typing and kinding disciplines allow for powerful forms of type reflection, ad-hoc polymorphism and type-directed meta-programming, which are often found in modern software development, but not typically expressible in a type-safe manner in general purpose languages. We validate our approach both formally and pragmatically by establishing the standard meta-theoretical results of type safety and via a prototype implementation of a kind checker, type checker and interpreter for our language.

(joint work with Luís Caires, presented at OOPSLA’19)

Bio:
Bernardo Toninho is an Assistant Professor at Faculdade de Ciências e Tecnologia, Universidade Nova de Lisboa and an integrated member of the PLASTIC research group at NOVA LINCS. His research focuses on language-based techniques applied to the development of more robust and safer computational systems, with an emphasis on concurrent and distributed systems. More specifically, his work is framed within the realm of advanced type theories (e.g. substructural type theories and dependent type theories) and their application to real-world programming and verification problems.
Bernardo has a PhD in Computer Science by Carnegie Mellon University and Universidade Nova de Lisboa (dual degree) on the logical foundations of session-based concurrent computation, MSc in Computer Science from CMU and FCT-UNL and a BSc in Computer Science from FCT-UNL.