The Experts below are selected from a list of 31443 Experts worldwide ranked by ideXlab platform
Lars Birkedal - One of the best experts on this subject based on the ideXlab platform.
-
a Logical Relation for monadic encapsulation of state proving contextual equivalences in the presence of runst
Symposium on Principles of Programming Languages, 2018Co-Authors: Amin Timany, Morten Kroghjespersen, Leo Stefanesco, Lars BirkedalAbstract:We present a Logical Relations model of a higher-order functional programming language with impredicative polymorphism, recursive types, and a Haskell-style ST monad type with runST. We use our Logical Relations model to show that runST provides proper encapsulation of state, by showing that effectful computations encapsulated by runST are heap independent. Furthermore, we show that contextual refinements and equivalences that are expected to hold for pure computations do indeed hold in the presence of runST. This is the first time such Relational results have been proven for a langauge with monadic encapsulation of state. We have formalized all the technical development and results in Coq.
-
a Relational model of types and effects in higher order concurrent separation logic
Symposium on Principles of Programming Languages, 2017Co-Authors: Morten Kroghjespersen, Kasper Svendsen, Lars BirkedalAbstract:Recently we have seen a renewed interest in programming languages that tame the complexity of state and concurrency through refined type systems with more fine-grained control over effects. In addition to simplifying reasoning and eliminating whole classes of bugs, statically tracking effects opens the door to advanced compiler optimizations. In this paper we present a Relational model of a type-and-effect system for a higher-order, concurrent program- ming language. The model precisely captures the semantic invariants expressed by the effect annotations. We demonstrate that these invariants are strong enough to prove advanced program transformations, including automatic parallelization of expressions with suitably disjoint effects. The model also supports refinement proofs between abstract data types implementations with different internal data representations, including proofs that fine-grained concurrent algorithms refine their coarse-grained counterparts. This is the first model for such an expressive language that supports both effect-based optimizations and data abstraction. The Logical Relation is defined in Iris, a state-of-the-art higher-order concurrent separation logic. This greatly simplifies proving well-definedness of the Logical Relation and also provides us with a powerful logic for reasoning in the model.
-
interactive proofs in higher order concurrent separation logic
Symposium on Principles of Programming Languages, 2017Co-Authors: Robbert Krebbers, Amin Timany, Lars BirkedalAbstract:When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they are cluttered with bookkeeping code related to manipulating the object logic. In this paper, we introduce a so-called proof mode that extends the Coq proof assistant with (spatial and non-spatial) named proof contexts for the object logic. We show that thanks to these contexts we can implement high-level tactics for introduction and elimination of the connectives of the object logic, and thereby make reasoning in the embedded logic as seamless as reasoning in the meta logic of the proof assistant. We apply our method to Iris: a state of the art higher-order impredicative concurrent separation logic. We show that our method is very general, and is not just limited to program verification. We demonstrate its generality by formalizing correctness proofs of fine-grained concurrent algorithms, derived constructs of the Iris logic, and a unary and binary Logical Relation for a language with concurrency, higher-order store, polymorphism, and recursive types. This is the first formalization of a binary Logical Relation for such an expressive language. We also show how to use the Logical Relation to prove contextual refinement of fine-grained concurrent algorithms.
-
a kripke Logical Relation for effect based program transformations
Information & Computation, 2016Co-Authors: Lars Birkedal, Filip Sieczkowski, Guilhem Jaber, Jacob ThamsborgAbstract:We present a Kripke Logical Relation for showing the correctness of program transformations based on a region-polymorphic type-and-effect system for an ML-like programming language with higher-order store and dynamic allocation. We also show how to use our model to verify a number of interesting program transformations that rely on effect annotations.In building the model, we extend earlier work by Benton et al. that treated, respectively dynamically allocated first-order references, and higher-order store for global variables. We utilize ideas from region-based memory management, and on Kripke Logical Relations for higher-order store.One of the key challenges that we overcome in the construction of the model is treatment of masking of regions (conceptually similar to deallocation). Our approach bears similarities to the one used in Ahmed's unary model of a region calculus in her Ph.D. thesis.
-
reasoning about object capabilities with Logical Relations and effect parametricity
IEEE European Symposium on Security and Privacy, 2016Co-Authors: Dominique Devriese, Lars Birkedal, Frank PiessensAbstract:Object capabilities are a technique for fine-grained privilegeseparation in programming languages and systems, with importantapplications in security. However, current formal characterisations donot fully capture capability-safety of a programming language and arenot sufficient for verifying typical applications. Usingstate-of-the-art techniques from programming languages research, wedefine a Logical Relation for a core calculus of JavaScript thatbetter characterises capability-safety. The Relation is powerfulenough to reason about typical capability patterns and supportsevolvable invariants on shared data structures, capabilities withrestricted authority over them and isolated components with restrictedcommunication channels. We use a novel notion of effect parametricityfor deriving properties about effects. Our results imply memory accessbounds that have previously been used to characterisecapability-safety.
Jacob Thamsborg - One of the best experts on this subject based on the ideXlab platform.
-
a kripke Logical Relation for effect based program transformations
Information & Computation, 2016Co-Authors: Lars Birkedal, Filip Sieczkowski, Guilhem Jaber, Jacob ThamsborgAbstract:We present a Kripke Logical Relation for showing the correctness of program transformations based on a region-polymorphic type-and-effect system for an ML-like programming language with higher-order store and dynamic allocation. We also show how to use our model to verify a number of interesting program transformations that rely on effect annotations.In building the model, we extend earlier work by Benton et al. that treated, respectively dynamically allocated first-order references, and higher-order store for global variables. We utilize ideas from region-based memory management, and on Kripke Logical Relations for higher-order store.One of the key challenges that we overcome in the construction of the model is treatment of masking of regions (conceptually similar to deallocation). Our approach bears similarities to the one used in Ahmed's unary model of a region calculus in her Ph.D. thesis.
-
a concurrent Logical Relation
Computer Science Logic, 2012Co-Authors: Lars Birkedal, Filip Sieczkowski, Jacob ThamsborgAbstract:We present a Logical Relation for showing the correctness of program transformations based on a new type-and-effect system for a concurrent extension of an ML-like language with higher-order functions, higher-order store and dynamic memory allocation. We show how to use our model to verify a number of interesting program transformations that rely on effect annotations. In particular, we prove a Parallelization Theorem, which expresses when it is sound to run two expressions in parallel instead of sequentially. The conditions are expressed solely in terms of the types and effects of the expressions. To the best of our knowledge, this is the first such result for a concurrent higher-order language with higher-order store and dynamic memory allocation.
-
a kripke Logical Relation for effect based program transformations
International Conference on Functional Programming, 2011Co-Authors: Jacob Thamsborg, Lars BirkedalAbstract:We present a Kripke Logical Relation for showing the correctness of program transformations based on a type-and-effect system for an ML-like programming language with higher-order store and dynamic allocation.We show how to use our model to verify a number of interesting program transformations that rely on effect annotations.Our model is constructed as a step-indexed model over the standard operational semantics of the programming language. It extends earlier work [7, 8]that has considered, respectively, dynamically allocated first-order references and higher-order store for global variables (but no dynamic allocation). It builds on ideas from region-based memory management [21], and on Kripke Logical Relations for higher-order store [12, 14].Our type-and-effect system is region-based and includes a region-masking rule which allows to hide local effects. One of the key challenges in the model construction for dynamically allocated higher-order store is that the meaning of a type may change since references, conceptually speaking, may become dangling due to region-masking. We explain how our Kripke model can be used to show correctness of program transformations for programs involving references that, conceptually, are dangling.
Derek Dreyer - One of the best experts on this subject based on the ideXlab platform.
-
the impact of higher order state and control effects on local Relational reasoning
Journal of Functional Programming, 2012Co-Authors: Derek Dreyer, Georg Neis, Lars BirkedalAbstract:Reasoning about program equivalence is one of the oldest problems in semantics. In recent years, useful techniques have been developed, based on bisimulations and Logical Relations, for reasoning about equivalence in the setting of increasingly realistic languages-languages nearly as complex as ML or Haskell. Much of the recent work in this direction has considered the interesting representation independence principles enabled by the use of local state, but it is also important to understand the principles that powerful features like higher-order state and control effects disable. This latter topic has been broached extensively within the framework of game semantics, resulting in what Abramsky dubbed the "semantic cube": fully abstract game-semantic characterizations of various axes in the design space of ML-like languages. But when it comes to reasoning about many actual examples, game semantics does not yet supply a useful technique for proving equivalences. In this paper, we marry the aspirations of the semantic cube to the powerful proof method of step-indexed Kripke Logical Relations. Building on recent work of Ahmed et al. (2009), we define the first fully abstract Logical Relation for an ML-like language with recursive types, abstract types, general references and call/cc. We then show how, under orthogonal restrictions to the expressive power of our language-namely, the restriction to first-order state and/or the removal of call/cc-we can enhance the proving power of our possible-worlds model in correspondingly orthogonal ways, and we demonstrate this proving power on a range of interesting examples. Central to our story is the use of state transition systems to model the way in which properties of local state evolve over time.
-
a kripke Logical Relation between ml and assembly
Symposium on Principles of Programming Languages, 2011Co-Authors: Chungkil Hur, Derek DreyerAbstract:There has recently been great progress in proving the correctness of compilers for increasingly realistic languages with increasingly realistic runtime systems. Most work on this problem has focused on proving the correctness of a particular compiler, leaving open the question of how to verify the correctness of assembly code that is hand-optimized or linked together from the output of multiple compilers. This has led Benton and other researchers to propose more abstract, compositional notions of when a low-level program correctly realizes a high-level one. However, the state of the art in so-called "compositional compiler correctness" has only considered relatively simple high-level and low-level languages.In this paper, we propose a novel, extensional, compiler-independent notion of equivalence between high-level programs in an expressive, impure ML-like λ-calculus and low-level programs in an (only slightly) idealized assembly language. We define this equivalence by means of a biorthogonal, step-indexed, Kripke Logical Relation, which enables us to reason quite flexibly about assembly code that uses local state in a different manner than the high-level code it implements (e.g. self-modifying code). In contrast to prior work, we factor our Relation in a symmetric, language-generic fashion, which helps to simplify and clarify the formal presentation, and we also show how to account for the presence of a garbage collector. Our approach relies on recent developments in Kripke Logical Relations for ML-like languages, in particular the idea of possible worlds as state transition systems.
-
the impact of higher order state and control effects on local Relational reasoning
International Conference on Functional Programming, 2010Co-Authors: Derek Dreyer, Georg Neis, Lars BirkedalAbstract:Reasoning about program equivalence is one of the oldest problems in semantics. In recent years, useful techniques have been developed, based on bisimulations and Logical Relations, for reasoning about equivalence in the setting of increasingly realistic languages - languages nearly as complex as ML or Haskell. Much of the recent work in this direction has considered the interesting representation independence principles enabled by the use of local state, but it is also important to understand the principles that powerful features like higher-order state and control effects disable. This latter topic has been broached extensively within the framework of game semantics, resulting in what Abramsky dubbed the "semantic cube": fully abstract game-semantic characterizations of various axes in the design space of ML-like languages. But when it comes to reasoning about many actual examples, game semantics does not yet supply a useful technique for proving equivalences. In this paper, we marry the aspirations of the semantic cube to the powerful proof method of step-indexed Kripke Logical Relations. Building on recent work of Ahmed, Dreyer, and Rossberg, we define the first fully abstract Logical Relation for an ML-like language with recursive types, abstract types, general references and call/cc. We then show how, under orthogonal restrictions to the expressive power our language - namely, the restriction to first-order state and/or the removal of call/cc - we can enhance the proving power of our possible-worlds model in correspondingly orthogonal ways, and we demonstrate this proving power on a range of interesting examples. Central to our story is the use of state transition systems to model the way in which properties of local state evolve over time.
-
a Relational modal logic for higher order stateful adts
Symposium on Principles of Programming Languages, 2010Co-Authors: Derek Dreyer, Georg Neis, Andreas Rossberg, Lars BirkedalAbstract:The method of Logical Relations is a classic technique for proving the equivalence of higher-order programs that implement the same observable behavior but employ different internal data representations. Although it was originally studied for pure, strongly normalizing languages like System F, it has been extended over the past two decades to reason about increasingly realistic languages. In particular, Appel and McAllester's idea of step-indexing has been used recently to develop syntactic Kripke Logical Relations for ML-like languages that mix functional and imperative forms of data abstraction. However, while step-indexed models are powerful tools, reasoning with them directly is quite painful, as one is forced to engage in tedious step-index arithmetic to derive even simple results. In this paper, we propose a logic LADR for equational reasoning about higher-order programs in the presence of existential type abstraction, general recursive types, and higher-order mutable state. LADR exhibits a novel synthesis of features from Plotkin-Abadi logic, Godel-Lob logic, S4 modal logic, and Relational separation logic. Our model of LADR is based on Ahmed, Dreyer, and Rossberg's state-of-the-art step-indexed Kripke Logical Relation, which was designed to facilitate proofs of representation independence for "state-dependent" ADTs. LADR enables one to express such proofs at a much higher level, without counting steps or reasoning about the subtle, step-stratified construction of possible worlds.
Francesco Gavazzo - One of the best experts on this subject based on the ideXlab platform.
-
on the versatility of open Logical Relations continuity automatic differentiation and a containment theorem
European Symposium on Programming, 2020Co-Authors: Gilles Barthe, Raphaelle Crubille, Ugo Dal Lago, Francesco GavazzoAbstract:Logical Relations are one among the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be immediately proved by means of Logical Relations, for instance program continuity and differentiability in higher-order languages extended with real-valued functions. Informally, the problem stems from the fact that these properties are naturally expressed on terms of non-ground type (or, equivalently, on open terms of base type), and there is no apparent good definition for a base case (i.e. for closed terms of ground types). To overcome this issue, we study a generalization of the concept of a Logical Relation, called open Logical Relation, and prove that it can be fruitfully applied in several contexts in which the property of interest is about expressions of first-order type. Our setting is a simply-typed \(\lambda \)-calculus enriched with real numbers and real-valued first-order functions from a given set, such as the one of continuous or differentiable functions. We first prove a containment theorem stating that for any collection of real-valued first-order functions including projection functions and closed under function composition, any well-typed term of first-order type denotes a function belonging to that collection. Then, we show by way of open Logical Relations the correctness of the core of a recently published algorithm for forward automatic differentiation. Finally, we define a refinement-based type system for local continuity in an extension of our calculus with conditionals, and prove the soundness of the type system using open Logical Relations.
Federico Laudisa - One of the best experts on this subject based on the ideXlab platform.
-
counterfactual reasoning realism and quantum mechanics much ado about nothing
Erkenntnis, 2019Co-Authors: Federico LaudisaAbstract:I show why old and new claims on the role of counterfactual reasoning for the EPR argument and Bell’s theorem are unjustified: once the Logical Relation between locality and counterfactual reasoning is clarified, the use of the latter does no harm and the nonlocality result can well follow from the EPR premises. To show why, after emphasizing the role of incompleteness arguments that Einstein developed before the EPR paper, I critically review more recent claims that equate the use of counterfactual reasoning with the assumption of a strong form of realism and argue that such claims are untenable.
-
counterfactual reasoning realism and quantum mechanics much ado about nothing
arXiv: Quantum Physics, 2017Co-Authors: Federico LaudisaAbstract:I purport to show why old and new claims on the role of counterfactual reasoning for the EPR argument and the Bell theorem are unjustified: once the Logical Relation between locality and counterfactual reasoning is clarified, the use of the latter does no harm and the nonlocality result can well follow from the EPR premises. To show why, I critically review (i) incompleteness arguments that Einstein developed before the EPR paper, and (ii) more recent claims that equate the use of counterfactual reasoning with the assumption of a strong form of realism.
