LogSem Seminar talks 2019-2016
09-09-2019: Epistemic Modal Logic and non-interference
Speaker: Jeppe Blaabjerg
Time: 13:00-15:00
Location: Nygaard meeting room 395
Abstract: I will be talking about Epistemic Modal Logic, applications and challenges, specifically regarding non-interference.
It will be based on the following material:
Book:
Reasoning About Knowledge (Fagin, Ronald and Halpern, Joseph Y. and Vardi, Moshe Y. and Moses, Yoram, 1995)
Articles:
Secrecy in Multiagent Systems (Joseph Y. Halpern and Kevin R. O’Neill, 2008) Epistemic Temporal Logic for Information Flow Security (Balliu, Musard and Dam, Mads and Le Guernic, Gurvan, 2011) Understanding and Enforcing Opacity (Schoepe, Daniel and Sabelfeld, Andrei, 2015)
Extended abstract: Knowledge and Effect: A Logic for Reasoning about Confidentiality and Integrity Guarantees (Scott Moore, Aslan Askarov and Stephen Chong, 2015)
16-09-2019: Mechanisation of a capability machine and logical relations in Iris
Speaker: Aïna Linn Georges
Time: 13:00-15:00
Location: Nygaard meeting room 395
Abstract: I will be talking about the mechanisation of a capability machine into Iris, and the mechanisation of a Logical Relation, defined by Skorstensgaard et. al., for reasoning about capability safety.
Lau Skorstensgaard et al., Reasoning About a Machine with Local Capabilities : https://link.springer.com/content/pdf/10.1007%2F978-3-319-89884-1_17.pdf
The Logical Relation is implemented using techniques for formalising LRs into Iris: https://iris-project.org/pdfs/2019-icfp-logrelcc-final.pdf https://gitlab.mpi-sws.org/iris/examples/tree/master/theories/logrel
18-09-2019: Dependent type theory with modalities, modes, and a right adjoint to the ∏-type
Speaker: Andreas Nuyts
Time: 11:00-12:00
Location: Nygaard meeting room 295
Abstract: In dependent type theory, types and data can depend on other types and data. It is often worthwhile to use annotations on dependencies (often called modalities) to keep track of how a dependency’s output varies with its input. This way, good behaviour of functions can emerge from their implementation and be automatically verified, rather than manually proven. Examples of modalities are: parametricity, irrelevance, ad hoc polymorphism, functor variance, necessity/possibility, intensionality/extensionality, axiomatic cohesion, globality (the flat modality), …
The existence of identity and composite functions, requires that their exist identity and composite modalities. The set of modalities is therefore traditionally framed as a monoid. Recent work reveals that it is more interesting to view them as the morphisms of a category, whose objects are called modes. Well-known stratified type systems can be explained in this framework, e.g. System Fω can be seen as a system with a mode of types and a mode of data. Licata, Shulman and Riley provide a general simply-typed framework with a number of applications. Our work on “Degrees of Relatedness” shows how modes can give us a better understanding of parametricity, irrelevance and ad hoc polymorphism.
A parallel track of research on internalizing presheaf semantics, which is very much WIP, converges with the above. Presheaf semantics have been used to model HoTT, parametricity, and directed type theory. However, internalizations of univalence, parametricity and directed univalence have relied on various different presheaf operators. We propose the right adjoint to the ∏-type over representable presheaves (such as the interval) as a key tool to internalizing presheaf semantics. Unfortunately, the typing rules for this right adjoint look rather unsettling. However, when we consider variables of representable types not as part of the context, but as part of the mode, a right adjoint to the ∏-type seems to fit the multimode framework rather well.
With the Menkar proof assistant, we intend to provide an implementation of the above. During implementation, we encountered some interesting difficulties related to internal mode and modality polymorphism. The implementation of Degrees of Relatedness is approaching usability, whereas the right adjoint to the ∏-type is on the todo-list.
23-09-2019: Dr Levy: or How I Learned to Stop Worrying and Love Effects
Speaker: Alex Kavvos
Time: 13:00-14:30
Location: Nygaard meeting room 395
Abstract: A thorough introduction to everything you need to know about call-by-push-value.
30-09-2019: From incremental computation to higher categories
Speaker: Mario Alvarez-Picallo
Time: 13:00-15:30
Location: Nygaard meeting room 395
Abstract: Incremental computation is a practical technique used to efficiently compute the value of a function on a changing input. It is particularly widespread in the evaluation of Datalog queries, where it is known as semi-naive evaluation. We present the notion of change actions, an abstract formalization of a datatype where computation can be incrementalized, and show some surprising connections of this setting with differential geometry, the calculus of finite differences, and higher category theory.
07-10-2019: Initial semantics
Speaker: Benedikt Ahrens
Time: 13:00-15:00
Location: Nygaard meeting room 395
Abstract: The concept of characterizing data structures through an initiality property is important in computer science, where it is known under the terms Initial Semantics and Algebraic Specification. One purpose of algebraic specification is abstraction. One the one hand, initiality only determines data only up to isomorphism and leaves room for different implementations with different computer-scientific properties. On the other hand, the initiality property precisely encapsulates an important interface of the data structure: recursion and induction, which allow one to define functions on the data and to reason about those functions. In this talk, I present joint work with Hirschowitz, Lafont, and Maggesi on initial semantics for untyped lambda calculi. I show some examples of translations between languages defined by the recursion principle obtained from initiality.
10-10-2019: Directed type theory and homotopy theory
Speaker: Paige North
Time: 16:15-17:00
Location: Aud. D3 (1531-215)
Abstract: In this talk, I will describe the development of a directed type theory which can be used to describe directed homotopy theory and category theory. At the core of this type theory is a `homomorphism’ type former whose terms are meant to represent homomorphisms or directed paths. Its rules are roughly analogous to those of Martin-Löf’s identity type. I will give an interpretation of this type former in the category of small categories which helps to elucidate its rules. I will also describe directed variants of weak factorization systems for interpreting this type theory in categories of directed spaces.
21-10-2019: Data Abstraction and Relational Program Logic
Speaker: David Naumann
Time: 13:00-14:00
Location: Nygaard meeting room 395
Abstract: In a paper published in 1972 Hoare articulated the fundamental notions of hiding invariants and simulations. Hiding: invariants on encapsulated data representations need not be mentioned in specifications that comprise the API of a module. Simulation: correctness of a new data representation and implementation can be established by proving simulation between the old and new implementations using a coupling relation defined on the encapsulated state. These results were formalized semantically and for a simple model of state, though the paper claimed this could be extended to encompass dynamically allocated objects.
In this talk I will present recent work in which the ideas are combined with the idea in Hoare’s 1969 paper: a logic of programs. For a sequential language with dynamically allocated shared mutable objects, we introduce a relational Hoare logic that formalizes encapsulation, hiding of invariants, and relating two implementations via coupling relations. Unary and relational specifications and verification conditions are expressed entirely within first order logic. The proof rules are shown sound with respect to a conventional operational semantics together with a form of product program that provides explicit representation for alignments of execution steps.
Joint work with Anindya Banerjee and Mohammad Nikouei
22-10-2019: Munta: A Verified Model Checker for Timed Automata
Speaker: Simon Wimmer (TU Munich)
Time: 13:00-14:00
Location: Nygaard meeting room 295
Abstract: Munta is a mechanically verified model checker for timed automata, a popular formalism for modeling real-time systems. Our goal is two-fold: first, we want to provide a reference implementation that is fast enough to test other model checkers against it on reasonably sized benchmarks; second, the tool should be practical enough so that it can easily be used for experimentation. Munta can be compiled to Standard ML or OCaml and additionally features a web-based GUI. Its modeling language has a simple semantics but provides the most commonly used timed automata modeling features.
We will give a short introduction to timed automata, present the tool, and discuss particular challenges that arose in the verification of the tool.
04-11-2019: Coq Coq Correct: Verification of Type Checking and Erasure for Coq, in Coq
Speaker: Matthieu Sozeau
Time: 13:00-14:00
Location: Nygaard meeting room 395
Abstract: Coq is built around a well-delimited kernel that perfoms typechecking for definitions in a variant of the Calculus of Inductive Constructions (CIC). Although the metatheory of CIC is very stable and reliable, the correctness of its implementation in Coq is less clear. Indeed, implementing an efficient type checker for CIC is a rather complex task, and many parts of the code rely on implicit invariants which can easily be broken by further evolution of the code. Therefore, on average, one critical bug has been found every year in Coq. This paper presents the first implementation of a type checker for the kernel of Coq, which is proven correct in Coq with respect to its formal specification. Note that because of Gödel’s incompleteness theorem, there is no hope to prove completely the correctness of the specification of Coq inside Coq (in particular strong normalisation or canonicity), but it is possible to prove the correctness of the implementation assuming the correctness of the specification. Our work is based on the MetaCoq project [Anand et al. 2018; Sozeau et al. 2019] which provides metaprogramming facilities to work with terms and declarations at the level of this kernel. Our type checker is based on the specification of the typing relation of the Polymorphic, Cumulative Calculus of Inductive Constructions (PCUIC) at the basis of Coq and the verification of a relatively efficient and sound type-checker for it. In addition to the kernel implementation, an essential feature of Coq is so-called extraction [Letouzey 2004]: the production of executable code in functional languages from Coq definitions. We present a verified version of this subtle type-and-proof erasure step, therefore enabling the verified extraction of a safe type-checker for Coq.
Joint work with Simon Boulier, Yannick Forster, Théo Winterhalter and Nicolas Tabareau.
11-11-2019: Verification of functional smart contracts in Coq
Speaker: Danil Annenkov
Time: 13:00-14:00
Location: Nygaard meeting room 395
Abstract: I will introduce the notion of smart contracts for blockchains and briefly discuss existing smart contract languages. The focus will be on modern smart contract languages that tend to employ the functional programming paradigm. This fact makes functional smart contract languages perfect targets for embedding into proof assistants allowing for convenient reasoning about functional correctness. But we are also interested in the development of meta-theory of smart contract languages and would like to have strong guarantees about the correctness of the embedding. We implement our verification framework in Coq and use the meta-programming facilities of MetaCoq to have both deep (AST) and shallow (Coq functions) embeddings of a smart contract language. We prove a soundness theorem for our embedding and verify functional correctness properties of a crowdfunding contract. As an application of the developed framework, we show how to verify programs in Acorn - a functional smart contract language for the Concordium blockchain. The developed techniques could be applied to the verification of programs in various (not necessarily smart contract) functional languages.
Joint work with Bas Spitters and Jakob Botsch Nielsen.
18-11-2019: Smart Contract Interactions in Coq
Speaker: Jakob Botsch Nielsen
Time: 13:00-14:00
Location: Nygaard meeting room 395
Abstract: We present a model/executable specification of smart contract execution in Coq. Our formalization allows for inter-contract communication and generalizes existing work by allowing modelling of both depth-first execution blockchains (like Ethereum) and breadth-first execution blockchains (like Tezos). We represent smart contracts programs in Coq’s functional language Gallina, enabling easier reasoning about functional correctness of concrete contracts than other approaches. In particular, we develop a Congress contract in this style. This contract – a simplified version of the infamous DAO – is interesting because of its very dynamic communication pattern with other contracts. We give a high-level partial specification of the Congress’s behavior, related to reentrancy, and prove that the Congress satisfies it for all possible smart contract execution orders.
13-11-2019: Automated Verification of Parallel Nested DFS
Speaker: Marieke Huisman
Time: 9:00 - 10:00
Location: Nygaard meeting room 395
Abstract: Model checking algorithms are typically complex algorithms whose correctness is crucial for the usability of a model checker. However, establishing the correctness of such algorithms can be challenging, and is often done manually. This talk investigates how this verification process can be mechanized. This is urgently needed, because model-checking algorithms are often parallelized for efficiency reasons, which makes them even more error-prone.
In this talk, we show how the VerCors tool set can be used to mechanically verify the parallel nested depth first algorithm of Larman et al. We also show how having a mechanized proof supports the easy verification of various optimizations of the algorithm. As far as we are aware, this is the first deductive verification of a multi-core model checking algorithm.
(joint work with Wytse Oortwijn, Sebastiaan Joosten and Jaco van de Pol)
13-11-2019: Specifying and verifying liveness properties of the I/O behavior of programs in separation logic
Speaker: Bart Jacobs
Time: 10:00 - 11:00
Location: Nygaard meeting room 395
Abstract: We build on two lines of earlier work, on modular specification and verification of termination and safe I/O behavior, respectively, to obtain an approach for modular specification and verification of liveness properties of the I/O behavior of programs, such as the property that a server eventually responds to each request. Our approach reduces an “eventually X” property to a termination property, simply by imagining that X causes the program to terminate. To prove “eventually X and eventually Y”, we verify termination under the assumption that either X or Y (demonically chosen) causes termination.
25-11-2019: Linear Capabilities for Fully Abstract Compilation of Separation-Logic-Verified Code
Speaker: Thomas Van Strydonck
Time: 13:00 - 14:00
Location: Nygaard meeting room 395
Abstract: Separation logic is a powerful program logic for the static modular verification of imperative programs. However, dynamic checking of separation logic contracts on the boundaries between verified and untrusted modules is hard, because it requires one to enforce (among other things) that outcalls from a verified to an untrusted module do not access memory resources currently owned by the verified module. This paper proposes an approach to dynamic contract checking by relying on support for capabilities, a well-studied form of unforgeable memory pointers that enables fine-grained, efficient memory access control. More specifically, we rely on a form of capabilities called linear capabilities for which the hardware enforces that they cannot be copied. We formalize our approach as a fully abstract compiler from a statically verified source language to an unverified target language with support for linear capabilities. The key insight behind our compiler is that memory resources described by spatial separation logic predicates can be represented at run time by linear capabilities. The compiler is separation-logic-proof-directed: it uses the separation logic proof of the source program to determine how memory accesses in the source program should be compiled to linear capability accesses in the target program. The full abstraction property of the compiler essentially guarantees that compiled verified modules can interact with untrusted target language modules as if they were compiled from verified code as well.
02-12-2019: Modelling security - A cryptographer’s view of the world
Speaker: Sabine Oechsner
Time: 13:00 - 14:00
Location: Nygaard meeting room 395
** Abstract **: In this talk, I will try to provide some insight to non-cryptographers into how (a lot of) cryptographers think about and define security. After on overview of the objects and security intuitions studied, I will present the two standard approaches for defining security, game-based and simulation-based security, and discuss how to use them.
09-12-2019: mCoq: Mutation Analysis of Verification Projects
Speaker: Karl Palmskog
Time: 13:00 - 14:00
Location: Nygaard meeting room 395
Abstract: Mutation analysis, which introduces artificial defects into software systems, is the basis of mutation testing, a technique widely applied to evaluate and enhance the quality of test suites. However, despite the deep analogy between tests and formal proofs, mutation analysis has seldom been considered in the context of deductive verification.
In this talk, I will introduce mutation proving, a technique for analyzing verification projects that use proof assistants. Our implementation of mutation proving, a tool dubbed mCoq, applies a set of mutation operators to definitions of functions and datatypes in the Gallina language of the Coq proof assistant, inspired by operators previously proposed for functional programming languages. mCoq then checks proofs of lemmas affected by operator application.
We applied mCoq to 12 medium and large scale Coq projects, and recorded whether proofs passed or failed when applying different mutation operators. We then qualitatively analyzed the mutants, and found several examples of weak and incomplete specifications manifested as mutants that were live, i.e., for which all proofs passed. Based on our evaluation, we believe mCoq can be useful both to proof engineers for improving the quality of their verification projects and to researchers for evaluating proof engineering techniques.
Joint work with Ahmet Celik (Facebook), Marinela Parovic (University of Cambridge), Emilio Jésus Gallego Arias (INRIA), and Milos Gligoric (UT Austin).
16-12-2019: A hands-on tutorial on cubical Agda
Speaker: Zesen Qian
Time: 13:00 - 14:00
Location: Nygaard meeting room 395
Abstract: In this talk, I will give a hands-on tutorial of cubical Agda. We will talk about the motivation of cubical type theory and the basics from a computer science perspective. As a demonstration, we will prove group univalence (isomorphic groups are equal) in cubical Agda.
27-08-2018: The Call-by-Name Forcing Translation in Template Coq
Speaker: Danil Annenkov
Time: 14:00-15:00
Location: Nygaard meeting room 298
Abstract:
This talk presents an ongoing work on implementing a call-by-name forcing translation using the metaprograming facilities of Template Coq. The forcing translation allows for extending the type theory of Coq with new logical principles. This can be seen as a continuation of the work described in The Definitional Side of the Forcing by Jaber et al. We compare call-by-name and call-by-value translations and consider example applications: the “later” modality and cubical type theory.
27-08-2018: Language for specifying contracts
Speaker: Hans Bugge Grathwohl
Time: 13:00-14:00
Location: Nygaard meeting room 298
Abstract:
At Deon Digital we are developing a language for specifying contracts, and a system for monitoring the execution of these contracts on distributed ledgers. A contract can be thought of as a set of allowable chains of events, much like how a regular expression is a set of strings. This is in opposition to the so-called smart contracts of, e.g., Ethereum, which not only specify which events are allowed to happen, but also contain the strategies for executing the events.
I will talk about the design of the language and our goal of having a formalised semantics which hopefully can be used for automatic reasoning about properties of the contracts. Furthermore I can talk a bit about realistic use cases, and give a demo.
20-06-2018: Triangulating Context Lemmas
Speaker: Craig McLaughlin
Time: 14:00-16:00
Location: Turing 230 meeting room
Abstract:
This talk will give a general overview of my research and then focus on my recent work on context lemma results. The talk will touch on work that I conducted jointly with Sam Lindley and Conor McBride, and James McKinna and Ian Stark, respectively.
The idea of a context lemma spans a range of programming-language models from Milner’s original through the CIU theorem to ‘CIU-like’ results for multiple language features. Each shows that to prove observational equivalence between program terms it is enough to test only some restricted class of contexts: applicative, evaluation, reduction, etc.
We formally reconstruct a distinctive proof method for context lemmas based on cyclic inclusion of three program approximations: by triangulating between ‘applicative’ and ‘logical’ relations we prove that both match the observational notion, while being simpler to compute. Moreover, the observational component of the triangle condenses a series of approximations covering variation in the literature around what variable-capturing structure qualifies as a ‘context’.
All this is formalised in Agda: building on work of Allais et al., we specify lambda-calculus terms as well-typed and well-scoped by construction.
28-05-2018: COVERN: A Logic for Compositional Verification of Information Flow Control
Speaker: Johan Bay
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
I will talk about a paper by Toby Murray, Robert Sison and Kai Engelhardt which was presented at EuroS&P 2018. Link to paper.
14-05-2018: Towards a distributed programming language with dynamic information flow control
Speaker: Aslan Askarov
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
I will present an ongoing work on building an Erlang-like programming language for distributed systems with dynamic information flow control. I will describe the design and implementation of the prototype compiler and security-enforcing runtime together with a number of characteristic examples. Time permitting, I will also talk about the overall design of the system including the formal security guarantees that we target to prove. Joint work w/ Johan Bay.
07-05-2018: Things worth proving about the simply typed lambda-calculus
Speaker: Ranald Clouston
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
I will show how to do some basic syntactic proofs about the simply typed lambda-calculus, and argue that understanding the details of these basic lemmas can be essential to not making mistakes in the design of calculi with more advanced features.
30-04-2018: Internal Models of Cubical Type Theory
Speaker: Ian Orton
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
Cubical type theory is an extension of Martin-Löf type theory where the univalence axiom is a theorem. In this talk I present an approach to analysing models of cubical type theory using the internal language of a topos. I will explain the advantages that this method provides, discuss some of its limitations, and explain how we can overcome these limitations by extending the internal language with a modal operator.
23-04-2018: An Example of a Scalable Event-Driven Microservice
Speaker: Kasper Svendsen
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
In this talk I will present a realistic example of the architecture of a scalable event-driven microservice, based on the principles of event sourcing and CQRS.
19-04-2018: Resource Analysis for Probabilistic Programs
Speaker: Jan Hoffmann
Time: 14:00-15:00
Location: Nygaard meeting room 295
Abstract:
This talk presents a new static analysis for deriving upper bounds on the expected resource consumption of probabilistic programs. The analysis is fully automatic and derives symbolic bounds that are multivariate polynomials of the inputs. The new technique combines manual state-of-the-art reasoning techniques for probabilistic programs with an effective method for automatic resource-bound analysis of deterministic programs. It can be seen as both, an extension of automatic amortized resource analysis (AARA) to probabilistic programs and an automation of manual reasoning for probabilistic programs that is based on weakest preconditions. An advantage of the technique is that it combines the clarity and compositionality of a weakest-precondition calculus with the efficient automation of AARA. As a result, bound inference can be reduced to off-the-shelf LP solving in many cases and automatically-derived bounds can be interactively extended with standard program logics if the automation fails. Building on existing work, the soundness of the analysis is proved with respect to an operational semantics that is based on Markov decision processes. The effectiveness of the technique is demonstrated with a prototype implementation that is used to automatically analyze 39 challenging probabilistic programs and randomized algorithms. Experimental results indicate that the derived constant factors in the bounds are very precise and even optimal for many programs.
16-04-2018: Proving Termination and Liveness Properties
Speaker: Thomas Dinsdale-Young
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
I will talk about some recent work on proving termination and liveness, and share my thoughts on the topic.
09-04-2018: ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
Speaker: Dan Frumin
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
We present ReLoC: a logic for proving refinements of programs in a language with higher-order state, fine-grained concurrency, poly- morphism and recursive types. The core of our logic is a judgement e ≾ e' : τ, which expresses that a program e refines a program e' at type τ. In contrast to earlier work on refinements for languages with higher-order state and concurrency, ReLoC provides type- and structure-directed rules for manipulating this judgement, whereas previously, such proofs were carried out by unfolding the judge- ment into its definition in the model. These more abstract proof rules make it simpler to carry out refinement proofs. Moreover, we introduce logically atomic relational specifications: a novel approach for relational specifications for compound expres- sions that take effect at a single instant in time. We demonstrate how to formalise and prove such relational specifications in ReLoC, allowing for more modular proofs. ReLoC is built on top of the expressive concurrent separation logic Iris, allowing us to leverage features of Iris such as invariants and ghost state. We provide a mechanisation of our logic in Coq, which does not just contain a proof of soundness, but also tactics for interactively carrying out refinements proofs. We have used these tactics to mechanise several examples, which demonstrates the practicality and modularity of our logic.
The paper is available here.
19-03-2018: (Towards?) encoding the ML^2 proof technique in Iris
Speaker: Mathias Vorreiter Pedersen
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
I will show how one can prove termination-insensitive noninterference in Iris by encoding the ML^2 proof technique from Information Flow Inference for ML by Pottier and Simonet.
05-03-2018: Logical Relations for Guarded Recursive Kinds without Step-Indexing
Speaker: Lars Birkedal
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
I will talk about a recent paper by Karl Crary and Danny Gratzer. The abstract of the paper follows.
We present a new technique for the construction of step-index-free logical relations for languages with complex recursive character. We use syntactic minimal invariance to construct an ultrametric space of relations on programs. This space, unlike prior spaces of semantic types, is dependent neither on counting execution steps nor on a denotational semantics. As a result, we may take full advantage of the rich structure of the category of complete, 1-bounded ultrametric spaces for constructing logical relations that do not depend on execution traces. We demonstrate our approach by constructing a logical relation for a language with guarded recursive kinds that provides a sufficient foundation to encode general references via store passing.
26-02-2018: Iris with some support for linearity
Speaker: Aleš Bizjak
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
I will talk about some difficulties of managing resources in a logic such as Iris, and how to extend it to support more refined reasoning.
The talk is based on a draft paper.
19-02-2018: TLA+
Speaker: Morten Krogh-Jespersen
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
I will present TLA+ informally by going through the bakery-algorithm for mutual exclusion.
05-02-2018: Internal Universes in Models of Homotopy Type Theory
Speaker: Bas Spitters
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
When constructing categorical models of type theory it is often useful to work in the category’s internal language. However, we show that the universe in the Cohen-Coquand-Huber-M"ortberg (CCHM) model of homotopy type theory has an essentially global character – it cannot be described in the internal language of the topos of cubical sets. We get around this problem using the part of Shulman’s spatial type theory that extends the language of type theory with a modal operator for expressing properties of global (discrete) elements. In this setting we show how to construct a universe that is weakly generic for global CCHM fibrations starting from the assumption that the interval is tiny, which holds for cubical sets. This leads to a completely internal development of a model of homotopy type theory based upon the CCHM notion of fibration within what we call local type theory.
This is joint work with Dan Licata, Ian Orton, Andrew Pitts.
11-12-2017: A brief introduction to WebAssembly
Speaker: Lau Skorstengaard
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
In this talk I will present WebAssembly with an emphasis on the parts interesting for programming languages researchers.
04-12-2017: A Perspective on Specifying and Verifying Concurrent Modules
Speaker: Thomas Dinsdale-Young
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
I will give a talk based on a journal paper that I’ve recently been revising, with Pedro da Rocha Pinto and Philippa Gardner.
Abstract of the paper:
Specifying and verifying concurrent program modules are difficult problems. A specification should be general enough that any reasonable implementation satisfies it, yet precise enough that it can be used by any reasonable client. We survey a range of techniques for specifying concurrent modules, using the example of a counter module to illustrate the benefits and limitations of each. In particular, we highlight four key concepts underpinning these techniques: auxiliary state, interference abstraction, resource ownership and atomicity. We demonstrate how these concepts can be combined in a powerful approach to specifying and verifying concurrent modules.
27-11-2017: Mechanised Relational Verification of Concurrent Programs with Continuations
Speaker: Lars Birkedal
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
Concurrent higher-order imperative programming languages with continuations are very flexible and allow for the implementation of sophisticated programming patterns. For instance, researchers and practitioners have argued that the implementation of web servers can be simplified by using a programming pattern based on continuations. This programming pattern can, in particular, help simplify keeping track of the state of clients interacting with the server. However, such advanced programming programming languages are very challenging to reason about.
In this paper we present the first completely formalized tool for interactive mechanized relational verification of programs written in a concurrent higher-order imperative programming language with continuations (call/cc and throw). In more detail, we develop a novel logical relation which can be used to give mechanized proofs of contextual refinement. We use our method on challenging examples and prove, e.g., that a rudimentary web server implemented using the continuation-based pattern is contextually equivalent to one implemented without the continuation-based pattern.
20-11-2017: Analysis of resource usage
Speaker: Johan Bay and Mathias Vorreiter Pedersen
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
The second half of our series on RAML will consist of three sections:
- We will discuss how to bound resource consumption by multivariate polynomials.
- Then, we will briefly talk about growing the source language to full OCaml
- Finally, we will extend the ideas to capture relational cost analysis
The talk will consist of material from the following papers:
- Multivariate Amortized Resource Analysis
- Towards Automatic Resource Bound Analysis for OCaml
- Relational Cost Analysis
13-11-2017: Analysis of resource usage
Speaker: Johan Bay and Mathias Vorreiter Pedersen
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
In this first of two talks, we will look at Resource Aware ML (RAML) and discuss how it bounds resource usage using linear and univariate polynomials. We will look at the material from the following papers:
30-10-2017 and 31-10-2017: Nominal Cubical
Speaker: Andy Pitts
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
Models of various kinds of dependent type theory very frequently use particular presheaf toposes, that is, categories of set-valued functors out of a small category of “possible worlds”. Although the semantics of Type Theory in such a categories is pleasingly concrete, the Kripke-style quantification over possible worlds can become quite irksome. In particular cases it is possible instead to get a simpler formulation using an equivalent topos of finitely supported M-valued sets for a monoid M of substitutions.
In these lectures I will begin with something that may be of general use: a concrete description of the structures of the topos of M-valued sets (for an arbitrary monoid M) and its associated Category with Families that are relevant to interpreting Type Theory.
Then I will specialise to a particular monoid whose finitely supported M-sets are known to be equivalent to the cubical sets in the recent model of univalent foundations by Coquand-Cohen-Huber-Mörtberg (CCHM). Here there is a strong connection with the nominal techniques pioneered by Gabbay and myself. In particular, names in this setting are names of cartesian dimensions and name-abstraction gives the notion of path that plays a crucial role in the CCHM model. The full details of how these finitely supported M-sets model Voevodsky’s univalence axiom have yet to be worked out: I will see how far we can get, depending upon the stamina and assistance of the audience.
23-10-2017: Fitch-Style Modal Lambda Calculi
Speaker: Ranald Clouston
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
Fitch-style modal deduction, in which modalities are eliminated by opening a subordinate proof, and introduced by shutting one, were investigated in the 1990s as a basis for lambda calculi. We show that such calculi have good computational properties for a variety of intuitionistic modal logics, and are particularly suited for handling multiple necessity modalities. Semantics are given in cartesian closed categories equipped with an adjunction of endofunctors, with the necessity modality interpreted by the right adjoint. Where this functor is an idempotent comonad, a coherence result on the semantics allows us to present a calculus for intuitionistic S4 that is simpler than others in the literature. We show the calculi can be extended à la tense logic with the left adjoint of necessity, and are then complete for the categorical semantics.
02-10-2017: Program Tailoring: Slicing by Sequential Criteria
Speaker: Yue Li
Time: 14:00-15:00
Location: Nygaard meeting room 295
Abstract:
Protocol and typestate analyses often report some sequences of statements ending at a program point P that needs to be scrutinized, since P may be erroneous or imprecisely analyzed. Program slicing focuses only on the behavior at P by computing a slice of the program affecting the values at P. In this paper, we propose to restrict our attention to the subset of that behavior at P affected by one or several statement sequences, called a sequential criterion (SC). By leveraging the ordering information in a SC, e.g., the temporal order in a few valid/invalid API method invocation sequences, we introduce a new technique, program tailoring, to compute a tailored program that comprises the statements in all possible execution paths passing through at least one sequence in SC in the given order. With a prototyping implementation, Tailor, we show why tailoring is practically useful by conducting two case studies on seven large real-world Java applications. For program debugging and understanding, Tailor can complement program slicing by removing SC-irrelevant statements. For program analysis, Tailor can enable a pointer analysis, which is unscalable to a program, to perform a more focused and therefore potentially scalable analysis to its specific parts containing hard language features such as reflection.
02-10-2017: Efficient and Precise Points-to Analysis: Modeling the Heap by Merging Equivalent Automata
Speaker: Tian Tan
Time: 15:00-16:00
Location: Nygaard meeting room 295
Abstract:
Mainstream points-to analysis techniques for object-oriented languages rely predominantly on the allocation-site abstraction to model heap objects. We present MAHJONG, a novel heap abstraction that is specifically developed to address the needs of an important class of type-dependent clients, such as call graph construction, devirtualization and may-fail casting. By merging equivalent automata representing type-consistent objects that are created by the allocation-site abstraction, MAHJONG enables an allocation-site-based points-to analysis to run significantly faster while achieving nearly the same precision for type-dependent clients.
MAHJONG is simple conceptually, efficient, and drops easily on any allocation-site-based points-to analysis. We demonstrate its effectiveness by discussing some insights on why it is a better alternative of the allocation-site abstraction for type-dependent clients and evaluating it extensively on 12 large real-world Java programs with five context-sensitive points-to analyses and three widely used type-dependent clients. MAHJONG is expected to provide significant benefits for many program analyses where call graphs are required.
18-09-2017: Cumulative inductive types in Coq
Speaker: Amin Timany
Time: 14:00-16:00
Location: Nygaard meeting room 295
Abstract:
Having the type of all types in a type system results in paradoxes like Russel’s paradox. Therefore type theories like predicative calculus of inductive constructions (pCIC) – the logic of the Coq proof assistant – have a hierarchy of types Type₀, Type₁, Type₂, etc, where Type₀ : Type₁, Type₁ : Type₂, etc. In a cumulative type system, e.g., pCIC, for a term t such that t : Typeᵢ we also have that t : Type_{i+1}. The system pCIC has recently been extended to support universe polymorphism, i.e., definitions can be parametrized by universe levels. This extension does not support cumulativity for inductive types. For example, we do not have that a pair of types at levels i and j is also considered a pair of types at levels i+1 and j +1.
In this talk, I will discuss making inductive types cumulative in pCIC. Having inductive types be cumulative alleviates some problems that occur while working with large inductive types, e.g., the category of small categories, in pCIC.
12-06-2017: Caper: Under the Hood (part 2)
Speaker: Kristoffer Just Andersen
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
Look at the higher-level aspects of how Caper’s symbolic execution works.
22-05-2017: Caper: Under the Hood (part 1)
Speaker: Thomas Dinsdale Young
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
I will talk about Caper, a tool for automatic verification for fine-grained concurrency. I’ll give a high-level overview of the tool – what it does and how it works – before going into details of how it’s implemented and lessons we’ve learnt. In this part, I will talk about low-level infrastructure including:
- parsing and Caper’s lazy approach to type checking/inference
- the prover infrastructure
- interfacing to SMT solvers and other provers
- the monad stack
Previous talks
15-05-2017: From trash to treasure: timing-sensitive garbage collection
Speaker: Mathias Vorreiter Pedersen
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
This paper studies information flows via timing channels in the presence of automatic memory management. We construct a series of example attacks that illustrate that garbage collectors form a shared resource that can be used to reliably leak sensitive information at a rate of up to 1 byte/sec on a contemporary general-purpose computer. The created channel is also observable across a network connection in a datacenter-like setting. We subsequently present a design of automatic memory management that is provably resilient against such attacks.
This is a practice talk for the upcoming presentation at S&P 2017.
24-04-2017: Towards a proof of active security for multi-party computation in easycrypt
Speaker: Bas Spitters
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
We are formalizing a secret sharing scheme in the easycrypt proof assistant and apply it to a Multi-Party Computation (MPC) protocol. Easycrypt is an interactive theorem prover based on probabilistic relational hoare logic with a powerful automatic SMT backend. It thus allows to specify protocols in a precise probabilistic While language, and to reasoning about adversaries by using an ML-like module system. One states precise invariants about this protocol and finally proves these in a tactic-based way.
We show that the easycrypt methodology works for MPC. We replace simulation based proofs by non-interference proofs. Generally, we highlight how to do security proofs by showing the equivalence of imperative and functional code. The latter makes clear link to the verification of programming languages.
This is a progress report on a project that grew out of the Computer Aided Security course by Aslan Askarov and Bas Spitters and is joint work with Helen Haagh, Aleksandr Karbyshev, Sabine Oechsner, and Pierre-Yves Strub.
03-04-2017: Linking Types for Multi-Language Software: Have Your Cake and Eat It Too
Speaker: Lau Skorstengaard
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
I will present the paper Linking Types for Multi-Language Software: Have Your Cake and Eat It Too by Daniel Patterson and Amal Ahmed.
Paper abstract follows.
Software developers compose systems from components written in many different languages. A business-logic component may be written in Java or OCaml, a resource-intensive component in C or Rust, and a high-assurance component in Coq. In this multi-language world, program execution sends values from one linguistic context to another. This boundary-crossing exposes values to contexts with unforeseen behavior—that is, behavior that could not arise in the source language of the value. For example, a Rust function may end up being applied in an ML context that violates the memory usage policy enforced by Rust’s type system. This leads to the question of how developers ought to reason about code in such a multi-language world where behavior inexpressible in one language is easily realized in another.
This paper proposes the novel idea of linking types to address the problem of reasoning about single-language components in a multi-lingual setting. Specifically, linking types allow programmers to annotate where in a program they can link with components inexpressible in their unadulterated language. This enables developers to reason about (behavioral) equality using only their own language and the annotations, even though their code may be linked with code written in a language with more expressive power.
27-03-2017: Explicit Secrecy: A Policy for Taint Tracking
Speaker: Mathias Vorreiter Pedersen
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
I’ll be presenting the paper Explicit Secrecy: A Policy for Taint Tracking.
Abstract of the paper follows.
Taint tracking is a popular security mechanism for tracking data-flow dependencies, both in high-level languages and at the machine code level. But despite the many taint trackers in practical use, the question of what, exactly, tainting means—what security policy it embodies—remains largely unexplored.
We propose explicit secrecy, a generic framework capturing the essence of explicit flows, i.e., the data flows tracked by tainting. The framework is semantic, generalizing previous syntactic approaches to formulating soundness criteria of tainting. We demonstrate the usefulness of the framework by instantiating it with both a simple high-level imperative language and an idealized RISC machine. To further understanding of what is achieved by taint tracking tools, both dynamic and static, we obtain soundness results with respect to explicit secrecy for the tainting engine cores of a collection of popular dynamic and static taint trackers.
20-03-2017: Compositional Shape Analysis by means of Bi-Abduction
Speaker: Kristoffer Just Andersen
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
I’ll be presenting the paper “Compositional Shape Analysis by means of Bi-Abduction” by Calcagno et al. It can be found here.
20-03-2017: Internship report
Speaker: Felix Wiemuth
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
We want to analyse anonymity in various network protocols to eventually propose techniques that guarantee certain anonymity properties. To empirically evaluate those techniques in different scenrios, we designed a simple (mostly functional) language with native constructs for simulated networking. Anonymity is modelled by an anonymity parameter for each message, a set of possible senders the receiver will see.
As a realistic means of providing anonymity to its nodes, the simulated network provides participants with anonymous identities: Nodes can request symbolic addresses which will forward messages to them but are otherwise unlinked to their real identity (address).
Furthermore the language features a sandbox mode allowing network nodes to execute untrusted code (such as code received over the network) in an environment where critical calls (as to network functionality) are proxied by user-defined functions. This bans the otherwise possible leakage of identity through 3rd party code.
The implementation, an interpreter written in haskell, outputs logs of network activity which is used as a basis for statistical anonymity analyses. In practice, the interpreter could be used to test applications empirically for anonymity properties before running them in a real network like Tor. To this effect, the interpreter can be a basis for a compiler producing real world code (like Javascript) for the empirically verified code.
06-03-2017: Semantics of probabilistic programming languages
Speaker: Daniel Huang
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
In this talk, we will present some of our recent work on probabilistic programming languages. In the first half of the talk, we will describe a semantics for these languages based on Type-2 computable distributions. Such an approach enables us to reason denotationally about probabilistic programs as well as in terms of sampling. In the second half, we will describe a compiler for a simple probabilistic programming language. The compiler uses a sequence of intermediate languages to gradually and successively transform a specification of a probabilistic model into a Markov Chain Monte Carlo inference algorithm for execution on the CPU or GPU.
27-02-2017: The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time
Speaker: Ranald Clouston
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
I will talk about the paper The Many Worlds of Modal λ-calculi: I. Curry-Howard for Necessity, Possibility and Time. The abstract of the paper follows.
This is a survey of λ-calculi that, through the Curry-Howard isomorphism, correspond to constructive modal logics. We cover the prehistory of the subject and then concentrate on the developments that took place in the 1990s and early 2000s. We discuss logical aspects, modal λ-calculi, and their categorical semantics. The logics underlying the calculi surveyed are constructive versions of K, K4, S4, and LTL.
20-02-2017: Starling: Lightweight Concurrency Verification With Views
Speaker: Thomas Dinsdale Young
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
I will look at Starling, which is a tool for concurrency verification based on concurrent separation logic that is being developed by Matthew Windsor, Mike Dodds, Ben Simner and Matthew Parkinson. The most recent version of their paper (currently under review) is available here.
I will talk about how programs are specified and verified with Starling, and the theory behind it. Possibly we’ll also see it in action. I’ll also try to make some comparisons with Caper.
13-02-2017: A Split Model of Guarded Dependent Type Theory
Speaker: Aleš Bizjak
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
I will talk about my recent work with Rasmus Møgelberg on a split version of the model in our MFPS 2015 paper.
06-02-2017: A Calculus for Flow-Limited Authorization
Speaker: Aslan Askarov
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
I will talk about the paper A Calculus for Flow-Limited Authorization.
30-01-2017: The HoTT library: a formalization of homotopy type theory in Coq
Speaker: Bas Spitters
Time: 14:00-15:00
Location: Nygaard meeting room 295
Abstract:
I will repeat my CPP presentation of last week.
The HoTT library: a formalization of homotopy type theory in Coq
Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters.
Abstract of the paper.
We report on the development of the HoTT library, a formalization of homotopy type theory in the Coq proof assistant. It formalizes most of basic homotopy type theory, including univalence, higher inductive types, and significant amounts of synthetic homotopy theory, as well as category theory and modalities. The library has been used as a basis for several independent developments. We discuss the decisions that led to the design of the library, and we comment on the interaction of homotopy type theory with recently introduced features of Coq, such as universe polymorphism and private inductive types.
11-01-2017: Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
Speaker: Dexter Kozen
Time: 15:00-16:00
Location: Nygaard meeting room 395
Abstract:
NetKAT is a language/logic for specifying, programming, and reasoning about packet-switching networks. ProbNetKAT is a probabilistic extension of NetKAT with a compositional denotational semantics based on Markov kernels. The language is expressive enough to generate continuous distributions, which raises the question of how to compute effectively in the language. In this talk I will describe a new domain-theoretic characterization of the semantics, which provides the foundation needed to build a practical implementation. The new semantics allows the behavior of an arbitrary ProbNetKAT program to be approximated to arbitrary precision with distributions of finite support. There is a prototype implementation, which can be used to solve a variety of problems, including the calculation of the expected congestion induced by different routing schemes and reasoning probabilistically about reachability.
(joint work with Steffen Smolka, Nate Foster, Praveen Kumar, and Alexandra Silva)
19-12-2016: Tales of Belgium: Reasoning about Capability Machines using Logical Relations
Speaker: Lau Skorstengaard
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
In this talk, I will present the joint work I have been doing in Belgium with Dominique Devriese. The talk will consist of a presentation of capability machines and the formalisation we work with as well as a presentation of the logical relation we have developed to reason about programs on this capability machine.
12-12-2016: On Sessions and Infinite Data
Speaker: Ranald Clouston
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
We investigate some subtle issues that arise when programming distributed computations over infinite data structures. To do this, we formalise a calculus that combines a call-by-name functional core with session-based communication primitives and that allows session operations to be performed “on demand”. We develop a typing discipline that guarantees both normalisation of expressions and progress of processes and that uncovers an unexpected interplay between evaluation and communication.
This paper appears at COORDINATION 2016.
Link to the paper http://link.springer.com/chapter/10.1007/978-3-319-39519-7_15
5-12-2016: One-Dimensional Higher Inductive Types
Speaker: Peter Dybjer
Time: 15:00-16:00
Location: Nygaard meeting room 395
Abstract:
We present a general schema for one-dimensional higher inductive types, that is, higher inductive types with only point and path constructors. A general form for an introduction rule is proposed, as well as an inversion principle for deriving the elimination and equality rules from the introduction rules. We also show that the setoid model supports this schema. Finally, we outline the extension of this schema to two- dimensional higher inductive types.
5-12-2016: Programming Coinductive Proofs
Speaker: Brigitte Pientka
Time: 14:00-15:00
Location: Nygaard meeting room 395
Abstract:
Coinduction is one of the most basic concepts in computer science. Yet, reasoning coinductively about formal systems, representing their coinductive proofs, generating and manipulating such proofs is challenging and not commonly supported. In this talk, we develop the idea of programming coinductive proofs dual to the idea of programming inductive proofs. Unlike finite derivations which can be defined by constructing a proof tree, coinductive derivations are define by observations. Dual to pattern matching, a tool for analyzing finite data, we develop the concept of copattern matching, which allows us to synthesize infinite data. This leads to a symmetric language design where pattern matching on finite and infinite data can be mixed.
28-11-2016: Diagonal Arguments and Cartesian Closed Categories
Speaker: Mathias Høier
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
I will present the paper Diagonal Arguments and Cartesian Closed Categories by F. William Lawvere
The paper is available http://www.tac.mta.ca/tac/reprints/articles/15/tr15.pdf
It has no abstract, as it was originally a lecture note, but the introduction reads:
The similarity between the famous arguments of Cantor, Russell, Gödel and Tarski is well-known, and suggests that these arguments should all be special cases of a single theorem about a suitable kind of abstract structure. We offer here a fixed-point theorem in cartesian closed categories which seems to play this role.
21-11-2016: Towards a Quantitative Theory of Effects
Speaker: Radu Mardare
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
We develop a quantitative analogue of equational reasoning which we call quantitative algebraic reasoning. We define an indexed equality relation of type a =ₑ b which we think of as saying that “a is approximately equal to b up to an error of e”. The models are universal algebras defined on metric spaces. We have interesting examples where we have a quantitative equational theory whose free algebras correspond to well known structures. In each case we have finitary and continuous versions. The cases are: Hausdorff metrics from quantitive semilattices; p-Wasserstein metrics (hence also the Kantorovich metric) from barycentric algebras; and the total variation distance from a particular type of barycentric algebras.
This is a joint work with Gordon Plotkin and Prakash Panangaden; preliminary results have been presented at LICS2016.
14-11-2016: Cantor meets Scott: Domain-Theoretic Foundations for Probabilistic Network Programming
Speaker: Aleš Bizjak
Time: 14:00-15:00
Location: Nygaard meeting room 395
Abstract:
I will present the paper [[https://arxiv.org/abs/1607.05830|Cantor meets Scott: Domain-Theoretic Foundations for Probabilistic Network Programming]] will appear at POPL 2017. The abstract of the paper follows.
ProbNetKAT is a probabilistic extension of NetKAT with a denotational semantics based on Markov kernels. The language is expressive enough to generate continuous distributions, which raises the question of how to effectively compute in the language. This paper gives an alternative characterization of ProbNetKAT’s semantics using domain theory, which provides the foundations needed to build a practical implementation. The new semantics demonstrates that it is possible to analyze ProbNetKAT programs precisely using approximations of fixpoints and distributions with finite support. We develop an implementation and show how to solve a variety of practical problems including characterizing the expected performance of traffic engineering schemes based on randomized routing and reasoning probabilistically about properties such as loop freedom.
7-11-2016: A Game-Theoretic Approach to Concurrent Separation Logic
Speaker: Leo Stefanesco
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
I will present a new proof of the soundness of “classic” Concurrent Separation Logic using games: each Hoare triple induces a family of games, and the soundness is expressed as the existence of winning strategies. Joint work with Paul-André Melliès.
31-10-2016: A continuous model of type theory
Speaker: Chuangjie Xu
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
We introduce a constructive model of type theory validating Brouwer’s uniform-continuity principle, so that type-theoretic proofs with the principle as an assumption have computational content. For this, we develop a variation of Johnstone’s topological topos, which consists of sheaves on a certain uniform-continuity site that is suitable for predicative, constructive reasoning. Our concrete sheaves can be described as sets equipped with a suitable continuity structure, which we call C-spaces, and their natural transformations can be regarded as continuous maps. Our C-spaces form a locally cartesian closed category and hence give a model of dependent type theory. Moreover, the category has a fan functional that continuously compute moduli of uniform continuity, which validates the uniform-continuity principle formulated as a type via the Curry-Howard interpretation in dependent type theory.
24-10-2016: Compositional Noninterference for Concurrent Programs via Separation and Framing
Speaker: Aleksandr Karbyshev
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
Reasoning about information flow in a concurrent setting is notoriously difficult due in part to timing channels that may leak sensitive information. I will present a compositional type system for ensuring absence of leaks through the scheduler (internal timing) channel.
03-10-2016: Verifying a queue implementation in Iris
Speaker: Morten Krogh-Jespersen
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
In this talk I will discuss a queue implementation for the scheduler in the Fletch virtual machine, that supports enqueueing and dequeuing processes, but also stealing. I will propose a specification and show that the implementation satisfies said specification in Iris in Coq.
26-09-2016: Thoth: Comprehensive policy compliance in data retrieval systems
Speaker: Deepak Garg
Time: 14:00-15:00
Location: Nygaard meeting room 395
Abstract:
Data retrieval systems process data from many sources, each subject to its own data use policy. Ensuring compliance with these policies despite bugs, misconfiguration, or operator error in a large, complex, and fast evolving system is a major challenge. Thoth provides an efficient, kernel-level compliance layer for data use policies. Declarative policies are attached to the systems' input and output files, key-value tuples, and network connections, and specify the data’s integrity and confidentiality requirements. Thoth tracks the flow of data through the system at coarse-granularity, and enforces policy regardless of bugs, misconfigurations, compromises in application code, or actions by unprivileged operators. Thoth requires minimal changes to an existing system and has modest overhead, as we show using a prototype Thoth-enabled data retrieval system based on the popular Apache Lucene.
26-09-2016: Probability theory in Coq using synthetic topology, hopefully with an application to continuous probabilistic computation
Speakers: Florian Faissole and Bas Spitters
Time: 15:00-16:00
Location: Nygaard meeting room 395
Abstract:
We present the work of Florian’s internship on formalizing categorical probability theory in Coq. This is based on a small library for synthetic topology in HoTT, similar to synthetic (guarded) domain theory.
It is plausible that our development can serve as a basis for the semantics of continuous probabilistic computation in the spirit of easycrypt.
19-09-2016: From trash to treasure: timing-sensitive garbage collection
Speaker: Mathias Vorreiter Pedersen
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract: I will present our work on information flows via timing channels in the presence of automatic memory management. This will include:
A series of example attacks in Java and JavaScript that illustrate how garbage collectors form a shared resource that can be used to reliably leak sensitive information.
A design of automatic memory management that is provably resilient against the presented attacks.
12-09-2016: Simple Dependent Polymorphic I/O Effects
Speaker: Amin Timany
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
We give a short description of or work in progress on a very simple programming language, with a simple typing system that features explicit dependent and polymorphic I/O effects. This system having been inspired by type and effect systems [1] allows types to express what I/O operations the typed program possibly performs. The aim of this system is not to provide a way to prove functional correctness of programs with I/O effects [2] but rather demonstrate and argue that a simple type and effect system can allow us to get an upper bound on the I/O operations that a program performs.
- L. Birkedal, F. Sieczkowski, and J. Thamsborg. A Concurrent Logical Relation. In Computer Science Logic (CSL’12), 2012.
- W. Penninckx, B. Jacobs, and F. Piessens. Sound, modular and compositional verification of the input/output behavior of programs. In Programming Languages and Systems, April 2015.
05-09-2016: Caper and permissions
Speaker: Kristoffer Just Andersen
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
The monday talk will cover
- Permission accounting and it’s introduction in Caper
- The Readers-Writers problem
- (Part of) the internals of Caper and it’s handling of Guard resources
29-08-2016: Iris 3.0
Speaker: Robbert Krebbers
Time: 14:00-16:00
Location: Nygaard meeting room 395
Abstract:
In this talk I will give an introduction to Iris 3.0, which features:
- A small base logic with a simple model.
- The core concepts of the original Iris program logic – namely invariants, view shifts and the weakest precondition connective – are no longer defined in the model, but are formalized in the aforementioned base logic.
- Adequacy of the Iris program logic is proved from a very generic adequacy theorem for the base logic.
14-07-2016: The Lifetime Logic – A logic for Rust-style borrowing
Speaker: Ralf Jung from MPI-SWS Saarbrucken
Time: 14:00-15:00
Location: Nygaard meeting room 395
Abstract:
Rust is a modern safe systems programming language by Mozilla. It combines ease of use (taking quite some inspiration from Haskell) with blazing performance and low-level programming without sacrificing safety. Notably, even when the Rust type checker is too weak to understand safety of a library, the Rust type system is expressive enough for the library to provide a safe yet efficient interface to its clients. Our goal is to build a semantic model of the Rust type-system in order to prove safety of such “daring” libraries. A key difficulty there turns out to be Rust’s concept of “borrowing” pointers, for which we give a separation-logical account in Iris in the form of a novel “Lifetime Logic”.
20-06-2016: Caper: Automatic Verification with Concurrent Abstract Predicates
Speaker: Thomas Dinsdale-Young
Time: 14:00-15:00
Location: Nygaard meeting room 395
Abstract:
Recent developments have been made in program logics based on separation logic. These logics emphasise a modular approach to prove functional correctness for fine-grained concurrent programs, but have no automation support. I present Caper, a prototype tool for automated reasoning in such a logic, the logic of Concurrent Abstract Predicates (CAP). Caper is based on symbolic execution, integrating reasoning about interference on shared data and about ghost resources that are used to mediate this interference. This enables Caper to verify functional correctness of fine-grained concurrent algorithms.
13-06-2016: Dependent Types and Fibred Computational Effects
Speaker: Ranald Clouston
Time: 14:00-15:00
Location: Nygaard meeting room 395
Abstract:
I will present the paper Dependent Types and Fibred Computational Effects.
The abstract of the paper follows:
We study the interplay between dependent types and general computational effects. We define a language with both value types and terms, and computation types and terms, where types depend only on value terms. We use computational Σ-types to account for type-dependency in the sequential composition of computations. Our language design is justified by a natural class of categorical models. We account for both algebraic and non-algebraic effects. We also show how to extend the language with general recursion, using continuous families of cpos.
06-06-2016: CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization
Speaker: Lau Skorstengaard
Time: 14:00-15:00
Location: Nygaard meeting room 395
Abstract:
I will present the paper: “CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization”.
The abstract of the paper follows:
Abstract—CHERI extends a conventional RISC Instruction-Set Architecture, compiler, and operating system to support fine-grained, capability-based memory protection to mitigate memory-related vulnerabilities in C-language TCBs. We describe how CHERI capabilities can also underpin a hardware-software object-capability model for application compartmentalization that can mitigate broader classes of attack. Prototyped as an extension to the open-source 64-bit BERI RISC FPGA softcore processor, FreeBSD operating system, and LLVM compiler, we demonstrate multiple orders-of-magnitude improvement in scalability, simplified programmability, and resulting tangible security benefits as compared to compartmentalization based on pure Memory-Management Unit (MMU) designs. We evaluate incrementally deployable CHERI-based compartmentalization using several real-world UNIX libraries and applications.
02-06-2016: Programming and Proving with Concurrent Resources
Speaker: Ilya Sergey (University College London, UK)
Time: 13:00-14:00
Location: Nygaard meeting room 395
Abstract:
In the past decade, significant progress has been made towards design and development of efficient concurrent data structures and algorithms, which take full advantage of parallel computations. Due to sophisticated interference scenarios and a large number of possible interactions between concurrent threads, working over the same shared data structures, ensuring full functional correctness of concurrent programs is challenging and error-prone.
In my talk, through a series of examples, I will introduce Fine-grained Concurrent Separation Logic (FCSL)—a mechanized logical framework for implementing and verifying fine-grained concurrent programs.
FCSL features a principled model of concurrent resources, which, in combination with a small number of program and proof-level commands, is sufficient to give useful specifications and verify a large class of state-of-the-art concurrent algorithms and data structures. By employing expressive type theory as a way to ascribe specifications to concurrent programs, FCSL achieves scalability: even though the proofs for libraries might be large, they are done just once.
30-05-2016: Andromeda: handling extensional type theory
Speaker: Gaetan Gilbert
Time: 14:00-15:00
Location: Nygaard meeting room 395
Abstract:
Andromeda is an implementation of dependent type theory with equality reflection. The type theory is very expressive, as it allows one to postulate new judgmental equalities.
The design of Andromeda follows the tradition of LCF-style theorem provers:
- there is an abstract datatype of judgments,
- all constructions of judgments are done by a trusted nucleus and directly correspond to the inference rules of type theory (or easy derivations),
- the user interacts with the nucleus by writing programs in a high-level, statically typed meta-language Andromeda ML (AML).
The nucleus does not perform any normalization (it cannot as the underlying type theory has no normal forms), unification, or perform proof search. These techniques can all be implemented on top of the nucleus in AML, and therefore cannot produce invalid judgments.
Equality checking is delegated to the meta-level (equality checking in the underlying type theory is undecidable) by a mechanism of operations and handlers akin to those of the Eff programming language. Whenever the nucleus needs to check a non-trivial equation, it triggers an operation (question) which propagates to the meta-level. There it is intercepted by a user-defined handler which handles (answers) the equation by providing a witness for it.
23-05-2016: A Lambda-Calculus Foundation for Universal Probabilistic Programming
Speaker: Aleš Bizjak
Time: 14:00-15:00
Location: Nygaard meeting room 395
Abstract:
I will present parts of the paper “A Lambda-Calculus Foundation for Universal Probabilistic Programming” by Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak
The abstract of the paper follows:
We develop the operational semantics of an untyped probabilistic lambda-calculus with continuous distributions, as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our first contribution is to adapt the classic operational semantics of lambda-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integrating over all traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language.
10-05-2016: Environmental Bisimulations for Probabilistic Higher-Order Languages
Speaker: Valeria Vignudelli from University of Bologna, Italy
Time: 10:00 - 11:00
Location: Nygaard meeting room 395
Abstract:
The general topic of the talk are techniques for proving behavioural equivalence in languages with both probabilistic and higher-order operators. In particular, environmental bisimulations for probabilistic higher-order languages are studied. In contrast with applicative bisimulations, environmental bisimulations are known to be more robust and do not require sophisticated techniques such as Howe’s in the proofs of congruence. As representative calculi, probabilistic call-by-name and call-by-value lambda-calculus, and a probabilistic (call-by-value) lambda-calculus extended with references (i.e., a store) are considered. In each case full abstraction results are derived for probabilistic environmental similarity and bisimilarity with respect to contextual preorder and contextual equivalence, respectively. Some possible enhancements of the (bi)simulations, as ‘up-to techniques’, are also presented. Probabilities force a number of modifications to the definition of environmental bisimulations in non-probabilistic languages. Some of these modifications are specific to probabilities, others may be seen as general refinements of environmental bisimulations, applicable also to non-probabilistic languages.
This is a joint work with Davide Sangiorgi.
02-05-2016: Talk about “Verified Correctness and Security of OpenSSL HMAC”
Speaker: Aleksandr Karbyshev
Time: 14:00 - 15:00
Location: Nygaard meeting room 395
Abstract:
Talk about the paper “Verified Correctness and Security of OpenSSL HMAC” by Beringer, Petcher, Ye, Appel. The paper is available here: https://www.usenix.org/system/files/conference/usenixsecurity15/sec15-paper-beringer.pdf
25-04-2016: Fully abstract compilation by approximate back-translation
Speaker: Dominique Devriese KU Leuven, Belgium
Time: 14:00 - 15:00
Location: Nygaard meeting room 395
Abstract: A compiler is fully abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have important security benefits, as they limit the power of an attacker interacting with the program in the target language to that of an attacker interacting with the program in the source language. Proving compiler full-abstraction is, however, rather complicated. A common proof technique is based on the back-translation of target-level program contexts to behaviourally-equivalent source-level contexts. However, constructing such a back-translation is problematic when the source language is not strong enough to embed an encoding of the target language. For instance, when compiling from the simply-typed λ-calculus (λτ) to the untyped λ-calculus (λu), the lack of recursive types in λτ prevents such a back-translation. We propose a general and elegant solution for this problem. The key insight is that it suffices to construct an approximate back-translation. The approximation is only accurate up to a certain number of steps and conservative beyond that, in the sense that the context generated by the back-translation may diverge when the original would not, but not vice versa. Based on this insight, we describe a general technique for proving compiler full-abstraction and demonstrate it on a compiler from λτ to λu . The proof uses asymmetric cross-language logical relations and makes innovative use of step-indexing to express the relation between a context and its approximate back-translation. We believe this proof technique can scale to challenging settings and enable simpler, more scalable proofs of compiler full-abstraction.
Joint work with Marco Patrignani and Frank Piessens.
25-04-2016: Interactive separation logic proofs in Coq
Speaker: Robbert Krebbers
Time: 15:00 - 16:30
Location: Nygaard meeting room 395
Abstract: During this talk I will demonstrate the new Coq formalization of the Iris program logic. The new Coq formalization has the following features:
- A proof mode for doing interactive Iris proofs in a style that is very close to the style employed on paper.
- A significant performance improvement; compilation has improved by an order of magnitude.
- A more expressive logic, with a new feature we call higher-order ghost state.
These features have opened the way for using Coq not just to establish soundness and adequacy (as what happened in the original version of Iris), but to use it to prove properties of subtle higher-order concurrent programs.