An Introduction to Iris: Higher-Order Concurrent Separation Logic
- document 1 document 2 document 3
- niveau 1 niveau 2 niveau 3
- audio 1 audio 2 audio 3
Descriptif
In this talk I will give an introduction to our research on Iris, a logical framework, implemented and verified in the Coq proof assistant, which can be used for mathematical reasoning about safety and correctness of concurrent higher-order imperative programs.
Intervenants
Thèmes
Notice
Sur le même thème
-
-
Theoretical Foundations for Runtime MonitoringAcetoLuca
Runtime monitoring/verification is a lightweight technique that complements other verification methods in a multi-pronged approach towards ensuring software correctness. The technique poses novel
-
The Legacy of Rudolph KalmanWhiteStuart
In 1960 Rudolph Kalman published what is arguably the first paper to develop a systematic, principled approach to the use of data to improve the predictive capability of mathematical models. As our
-
On the notion of dimension of unimodular discrete spaces (workshop ERC Nemo Processus ponctuels et …
In this talk we will define notions of dimension for unimodular random graphs and point-stationary point processes. These notions are in spirit similar to the Minkowski dimension and the
-
A stable marriage between order and disorder (workshop ERC Nemo Processus ponctuels et graphes aléa…LastGünter
Stable matchings were introduced in a seminal paper by Gale and Shapley (1962) and play an important role in economics. Following closely Holroyd, Pemantle, Peres and Schramm (2009), we shall
-
Subdiffusivity of random walks on random planar maps, via stationarity (workshop ERC Nemo Processus…CurienNicolas
Random planar maps have been the subject of numerous studies over the last years. They are instance of stationary and reversible random planar maps exhibiting a non-conventional geometry at
-
Stein-Malliavin method for discrete alpha stable point processes (workshop ERC Nemo Processus ponct…DecreusefondLaurent
The notion of discrete alpha-stable point processes generalizes to point processes the notion of stable distribution. It has been introduced and studied by Davydov, Molchanov and Zuyev a few
-
Central Limit theorem for quasi-local statistics of point processes with fast decay of correlations…
We shall consider Euclidean stationary point processes which have fast decay of correlations i.e., their correlation functions factorize upto an additive error decaying exponentially in the
-
Eternal family trees and dynamics on unimodular random graphs (workshop ERC Nemo Processus ponctuel…Haji MirsadeghiMir Omid
This talk is centered on covariant dynamics on unimodular random graphs and random networks (marked graphs), namely maps from the set of vertices to itself which are preserved by graph or
-
Sampling cluster point processes: a review (workshop ERC Nemo Processus ponctuels et graphes aléato…BrémaudPierre
The theme of this talk is the sampling of cluster and iterated cluster point processes. It is partially a review, mainly of the Brix–Kendall exact sampling method for cluster point processes and
-
Absence of percolation for Poisson outdegree-one graphs (workshop ERC Nemo Processus ponctuels et g…CoupierDavid
A Poisson outdegree-one graph is a directed graph based on a marked Poisson point process such that each vertex has only one outgoing edge. We state the absence of percolation for such graphs
-
Strict monotonicity of percolation thresholds under covering maps (workshop ERC Nemo Processus ponc…MartineauSébastien
Percolation is a model for propagation in porous media that as introduced in 1957 by Broadbent and Hammersley. An infinite graph G models the geometry of the situation and a parameter p