P R O G R A M
The conference program will be available nearer to the start of the conference, please check back soon.
P R O G R A M
The conference program will be available nearer to the start of the conference, please check back soon.
Title:
Probabilistic Programming
Abstract:
Probabilistic programming refers to the idea of developing a programming language for writing and reasoning about probabilistic models from machine learning and statistics. Such a language comes with the implementation of several generic inference algorithms that answer various queries about the models written in the language, such as posterior inference and marginalisation. By providing these algorithms, a probabilistic programming language enables data scientists to focus on designing good models based on their domain knowledge, instead of building effective inference engines for their models, a task that typically requires expertise in machine learning, statistics and systems. Even experts in machine learning and statistics may get benefited from such a probabilistic programming system because using the system they can easily explore highly advanced models.
In the past four years, with colleagues from programming languages, machine learning and probability theory, I have worked on developing the semantic foundations, efficient inference algorithms, and static program analysis for such probabilistic programming languages, especially those that support expressive language features such as higher-order functions, continuous distributions and general recursion. In this talk, I will describe what I have learnt so far.
Sarah Winkler
Title:
Maximal Termination, More Proofs?
Equational Theorem Proving as an Optimization Problem
Abstract:
Maximal completion is a simple yet highly effective approach to classical Knuth-Bendix completion based on maximum satisfiability. In this talk we describe how it also gives rise to a competitive equational theorem prover, and investigate the extension to instantiation-based theorem proving. Particular focus is put on the role of termination techniques.
Amy Felty
Title:
A Linear Logical Framework in Hybrid
Abstract:
We present a linear logical framework implemented within the Hybrid system. Hybrid is designed to support the use of higher-order abstract syntax for representing and reasoning about formal systems, implemented in the Coq Proof Assistant. In this work, we extend the system with a linear specification logic, which provides infrastructure for reasoning directly about object languages with linear features. Our current work includes applications of this framework to proving properties of quantum programming languages, meta-theory of low-level abstract machine code, proof theory of focused linear sequent calculi, and modeling biological processes as transition systems and proving properties about them.
Beniamino Accattoli
Title: A Fresh Look at the Lambda Calculus
Abstract: The (untyped) lambda-calculus is an old topic, almost 90 years old. And yet—I’ll try to argue—its study is far from being over. The talk is a bird’s eye view of the questions I have worked on in the last few years: how to measure the complexity of lambda terms, how to decompose their evaluation, how to implement it, and how all this varies according to the evaluation strategy. The talk aims at inducing a new way of looking at an old topic, focussing on high-level issues and perspectives.