Robert Atkey
University of Strathclyde, Scotland
Dependent Types in Polynomial Time
Dependently Typed programming languages such as Agda and Idris2, and to some extent Coq and Lean, allow a "very strongly typed" kind of functional programming. Their expressive type systems allow programmers to write detailed specifications for their programs that constrain and guide the programming experience, and provide verified guarantees about program behaviour.
However, these specifications can only express extensional properties of programs -- properties relating the "what" of programs, but not the "how". For example, it is not possible to directly state that a particular function executes in polynomial time.
I will present an extension to dependent type theory, based on linear types, that allows expression of properties like "polynomial time" within the language. I'll explain how the system works, and how to prove its soundness. Finally, I'll explain some consequences of such a system, and the kinds of complexity theory we can build upon it.
Dr. Robert Atkey is a Senior Lecturer at the University of Strathclyde in Scotland. He is leader of the Mathematically Structured Programming group in the Computer and Information Sciences department there. Before starting at Strathclyde in 2015, he did a PhD at the University of Edinburgh, postdoctoral research at the Universities of Edinburgh and Strathclyde, and worked in industry on static analysis of concurrent Java. His research is primarily focused on programming languages and their application to resource constrained computing, verification, and scientific computing.
Victor Taelin
HVM
HVM: tudo sobre o compilador funcional do futuro
Baseado em um novo modelo computacional que compartilha das melhores características da Máquina de Turing e do Cálculo Lambda, desenvolvemos um runtime funcional ultra-eficiente que, em seu protótipo inicial, conseguiu se equiparar, e, em muitos casos, superar, o GHC, o compilador do Haskell, que é, atualmente, o mais eficiente no ramo. Nesse tutorial exclusivo, Taelin mostrará como a HVM foi implementada, desde sua base teórica até os detalhes de baixo nível da sua implementação. Não somente, também ensinaremos como utilizar a HVM para desenvolver algoritmos funcionais de alta performance, explorando tanto o seu paralelismo inerente, quanto seus ganhos assintóticos.
Desde os 11 anos apaixonado por programação, Victor Taelin foi um dos desenvolvedores do Ethereum, a segunda maior criptomoeda, e criador do Kind, a primeira linguagem de uso geral a incluir provas formais, e do HVM, a máquina virtual funcional mais rápida do mundo.