Modern programming languages like Kotlin or Rust have advanced features to statically ensure data and memory safety, like nullable and ownership types. Other languages like C, Erlang, Go, Haskell, Java, or Scala, have static analysis tools to help the developer detect at compile-time possible safety violations that might lead to run-time errors. Most of these, however, force the developer to adopt a defensive programming style, trying to cover all possible scenarios where things might go wrong. Nevertheless, bad things still happen, being a testimony of this the Jedis bug uncovered after 9 years in Jan 2018 (issue closed 14 months later), or the MonoX Finance smart contract vulnerability exploited in December 2021. Since many applications implement protocols, as not all functionalities are available all the time (e.g., one can only pop from a non-empty stack; write in a not full buffer), behavioural types are a natural way to model and validate code enforcing that only the correct sequences of actions are allowed to happen. Static type systems ensure protocol compliance and, in some conditions, completion. Tools to use them with functional, imperative, or O.-O. mainstream languages are available, but still not widely adopted.
Motivación: modelando entidades computacionales con máquinas de estados, bugs notorios por violaciones de protocolo, observación de que el testing no es suficiente. Type-safety: de qué trata, cómo conseguirla, estado de lenguajes conocidos como C, Go, Haskell, Java, Rust. Desde data-safety a protocol-safety: systemas de transiciones etiquetadas (labelled transition systems, LTS), usando LTS para modelar entidades computacionales, nociones de tipos de comportamiento (session types, contracts, typestates), tipos de comportamiento para lenguajes de programación convencionales. Sobre session types: sintaxis, semántica, subtipado, ejemplos; session types (ST) para lenguajes simples (funcionales y orientados a objetos). STs en lenguajes de programación convencionales: C, Erlang, Haskell, OCaml, Java, Scala, Rust. Multiparty ST: ejemplos y conceptos, herramientas MST. Mini-proyecto: un sistema de subasta.
se sugiere:
Familiaridad con lenguajes de programación.
Idealmente, conocimiento de C, y algún lenguaje al estilo Java.
Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T Vasconcelos, Nobuko Yoshida: Behavioral types in programming languages. Foundations and Trends in Programming Languages 3 (2-3), 95-230 (2016).
Simon Gay and António Ravara (editors): Behavioural Types: from Theory to Tools. CRC Press (2017).
Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, Gianluigi Zavattaro: Foundations of Session Types and Behavioural Contracts. ACM Comput. Surv. 49(1): 3:1-3:36 (2016).
Desarrollado por el Departamento de Computación, FCEyN, UBA