Lars Birkedal

CoRR, 2019

2018

A model of guarded recursion via generalised equilogical spaces.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2018

A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST.

[BibT_eX]

[DOI]

Amin Timany

Léo Stefanesco

Morten Krogh-Jespersen

Proc. ACM Program. Lang., 2018

Iris from the ground up: A modular foundation for higher-order concurrent separation logic.

[BibT_eX]

[DOI]

Ralf Jung

Jacques-Henri Jourdan

J. Funct. Program., 2018

On Models of Higher-Order Separation Logic.

[BibT_eX]

[DOI]

Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, 2018

StkTokens: Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities - Technical Report with Proofs and Details.

[BibT_eX]

[DOI]

Lau Skorstengaard

Dominique Devriese

CoRR, 2018

Compositional Non-interference for Concurrent Programs via Separation and Framing.

[BibT_eX]

[DOI]

Proceedings of the Principles of Security and Trust - 7th International Conference, 2018

ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency.

[BibT_eX]

[DOI]

Dan Frumin

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2018

2017

Trace Properties from Separation Logic Specifications.

[BibT_eX]

[DOI]

Thomas Dinsdale-Young

Guilhem Jaber

Nikos Tzevelekos

CoRR, 2017

A relational model of types-and-effects in higher-order concurrent separation logic.

[BibT_eX]

[DOI]

Morten Krogh-Jespersen

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Interactive proofs in higher-order concurrent separation logic.

[BibT_eX]

[DOI]

Amin Timany

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

The Essence of Higher-Order Concurrent Separation Logic.

[BibT_eX]

[DOI]

Ralf Jung

Jacques-Henri Jourdan

Proceedings of the Programming Languages and Systems, 2017

Caper - Automatic Verification for Fine-Grained Concurrency.

[BibT_eX]

[DOI]

Thomas Dinsdale-Young

Pedro da Rocha Pinto

Kristoffer Just Andersen

Proceedings of the Programming Languages and Systems, 2017

2016

Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2016

A Kripke logical relation for effect-based program transformations.

[BibT_eX]

[DOI]

Inf. Comput., 2016

Preface.

[BibT_eX]

[DOI]

Proceedings of the Thirty-second Conference on the Mathematical Foundations of Programming Semantics, 2016

The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2016

Higher-order ghost state.

[BibT_eX]

[DOI]

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Guarded Dependent Type Theory with Coinductive Types.

[BibT_eX]

[DOI]

Hans Bugge Grathwohl

Ranald Clouston

Proceedings of the Foundations of Software Science and Computation Structures, 2016

Reasoning about Object Capabilities with Logical Relations and Effect Parametricity.

[BibT_eX]

[DOI]

Dominique Devriese

Frank Piessens

Proceedings of the IEEE European Symposium on Security and Privacy, 2016

Transfinite Step-Indexing: Decoupling Concrete and Logical Steps.

[BibT_eX]

[DOI]

Filip Sieczkowski

Proceedings of the Programming Languages and Systems, 2016

Guarded Cubical Type Theory: Path Equality for Guarded Recursion.

[BibT_eX]

[DOI]

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

2015

A Model of PCF in Guarded Type Theory.

[BibT_eX]

[DOI]

Marco Paviotti

Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics, 2015

Compositional Verification Methods for Next-Generation Concurrency (Dagstuhl Seminar 15191).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2015

Step-Indexed Logical Relations for Probability (long version).

[BibT_eX]

[DOI]

CoRR, 2015

Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning.

[BibT_eX]

[DOI]

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages.

[BibT_eX]

[DOI]

Filip Sieczkowski

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

Programming and Reasoning with Guarded Recursion for Coinductive Types.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2015

Step-Indexed Logical Relations for Probability.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computation Structures, 2015

A Separation Logic for Fictional Sequential Consistency.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2015

2014

A Model of Countable Nondeterminism in Guarded Type Theory.

[BibT_eX]

[DOI]

Marino Miculan

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

Modular reasoning about concurrent higher-order imperative programs.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Impredicative Concurrent Abstract Predicates.

[BibT_eX]

[DOI]

Troels Christoffer Damgaard

Proceedings of the Programming Languages and Systems, 2014

2013

A step-indexed Kripke model of hidden state.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2013

An inductive characterization of matching in binding bigraphs.

[BibT_eX]

[DOI]

Arne J. Glenstrup

Robin Milner

Formal Aspects Comput., 2013

Step-Indexed Relational Reasoning for Countable Nondeterminism.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2013

Logical relations for fine-grained concurrency.

[BibT_eX]

[DOI]

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Views: compositional reasoning for concurrent programs.

[BibT_eX]

[DOI]

Thomas Dinsdale-Young

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes.

[BibT_eX]

[DOI]

Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency.

[BibT_eX]

[DOI]

Aaron Turon

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

Modular Reasoning about Separation of Concurrent Data Structures.

[BibT_eX]

[DOI]

Matthew J. Parkinson

Proceedings of the Programming Languages and Systems, 2013

Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library.

[BibT_eX]

[DOI]

Matthew J. Parkinson

Proceedings of the ECOOP 2013 - Object-Oriented Programming, 2013

2012

A relational realizability model for higher-order stateful ADTs.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2012

The impact of higher-order state and control effects on local relational reasoning.

[BibT_eX]

[DOI]

Georg Neis

J. Funct. Program., 2012

Two for the Price of One: Lifting Separation Logic Assertions

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

First steps in synthetic guarded domain theory: step-indexing in the topos of trees

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

Formalized Verification of Snapshotable Trees: Separation and Sharing.

[BibT_eX]

[DOI]

Proceedings of the Verified Software: Theories, Tools, Experiments, 2012

Charge! - A Framework for Higher-Order Separation Logic in Coq.

[BibT_eX]

[DOI]

Jesper Bengtson

Jonas Braband Jensen

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Fictional Separation Logic.

[BibT_eX]

[DOI]

Jonas Braband Jensen

Proceedings of the Programming Languages and Systems, 2012

A Concurrent Logical Relation.

[BibT_eX]

[DOI]

Filip Sieczkowski

Proceedings of the Computer Science Logic (CSL'12), 2012

First Steps in Synthetic Guarded Domain Theory.

[BibT_eX]

[DOI]

Proceedings of the Advances in Modal Logic 9, 2012

2011

Modular Verification of Linked Lists with Views via Separation Logic.

[BibT_eX]

[DOI]

Jonas Braband Jensen

Peter Sestoft

J. Object Technol., 2011

Step-Indexed Kripke Model of Separation Logic for Storable Locks.

[BibT_eX]

[DOI]

Alexandre Buisse

Proceedings of the Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, 2011

Nested Hoare Triples and Frame Rules for Higher-order Store

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2011

Logical Step-Indexed Logical Relations

[BibT_eX]

[DOI]

Amal Ahmed

Log. Methods Comput. Sci., 2011

Partiality, State and Dependent Types.

[BibT_eX]

[DOI]

Proceedings of the Typed Lambda Calculi and Applications - 10th International Conference, 2011

Step-indexed kripke models over recursive worlds.

[BibT_eX]

[DOI]

Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2011

Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - Second International Conference, 2011

A kripke logical relation for effect-based program transformations.

[BibT_eX]

[DOI]

Proceedings of the Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, 2011

A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2011

Step-Indexed Relational Reasoning for Countable Nondeterminism.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 2011

2010

The category-theoretic solution of recursive metric-space equations.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2010

Realisability semantics of parametric polymorphism, general references and recursive types.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2010

Verifying event-driven programs using ramified frame properties.

[BibT_eX]

[DOI]

Neel Krishnaswami

Jonathan Aldrich

Proceedings of TLDI 2010: 2010 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2010

A relational modal logic for higher-order stateful ADTs.

[BibT_eX]

[DOI]

Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2010

A Semantic Foundation for Hidden State.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2010

A Metric Model of Lambda Calculus with Guarded Recursion.

[BibT_eX]

[DOI]

Proceedings of the 7th Workshop on Fixed Points in Computer Science, 2010

Verifying Generics and Delegates.

[BibT_eX]

[DOI]

Neelakantan R. Krishnaswami

Matthew J. Parkinson

Proceedings of the ECOOP 2010, 2010

10351 Executive Summary - Modelling, Controlling and Reasoning About State.

[BibT_eX]

[DOI]

Proceedings of the Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, 2010

10351 Abstracts Collection - Modelling, Controlling and Reasoning About State.

[BibT_eX]

[DOI]

Proceedings of the Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, 2010

2009

Design patterns in separation logic.

[BibT_eX]

[DOI]

Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2009

Relational parametricity for references and recursive types.

[BibT_eX]

[DOI]

Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, 2009

Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Software Science and Computational Structures, 2009

Solutions of Generalized Recursive Metric-Space Equations.

[BibT_eX]

[DOI]

Proceedings of the 6th Workshop on Fixed Points in Computer Science, 2009

2008

Local reasoning about a copying garbage collector.

[BibT_eX]

[DOI]

John C. Reynolds

ACM Trans. Program. Lang. Syst., 2008

Relational Parametricity and Separation Logic.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2008

Hoare type theory, polymorphism and separation.

[BibT_eX]

[DOI]

J. Gregory Morrisett

J. Funct. Program., 2008

Higher-Order Separation Logic in Isabelle/HOLCF.

[BibT_eX]

[DOI]

Carsten Varming

Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics, 2008

Ynot: dependent types for imperative programs.

[BibT_eX]

[DOI]

Proceedings of the Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, 2008

A Simple Model of Separation Logic for Higher-Order Store.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 35th International Colloquium, 2008

A Realizability Model for Impredicative Hoare Type Theory.

[BibT_eX]

[DOI]

Greg Morrisett

Proceedings of the Programming Languages and Systems, 2008

On the Construction of Sorted Reactive Systems.

[BibT_eX]

[DOI]

Søren Debois

Thomas T. Hildebrandt

Proceedings of the CONCUR 2008 - Concurrency Theory, 19th International Conference, 2008

2007

BI-hyperdoctrines, higher-order separation logic, and abstraction.

[BibT_eX]

[DOI]

Bodil Biering

ACM Trans. Program. Lang. Syst., 2007

Domain-theoretical models of parametric polymorphism.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2007

Book Reviews.

[BibT_eX]

[DOI]

Troels Christoffer Damgaard

Stud Logica, 2007

Abstract Predicates and Mutable ADTs in Hoare Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2007

2006

Axiomatizing Binding Bigraphs.

[BibT_eX]

Nord. J. Comput., 2006

Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2006

Linear Abadi and Plotkin Logic.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2006

Matching of Bigraphs.

[BibT_eX]

[DOI]

Troels Christoffer Damgaard

Arne J. Glenstrup

Robin Milner

Proceedings of the Workshop on Graph Transformation for Concurrency and Verification, 2006

Polymorphism and separation in hoare type theory.

[BibT_eX]

[DOI]

Greg Morrisett

Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, 2006

Bigraphical Models of Context-Aware Systems.

[BibT_eX]

[DOI]

Søren Debois

Ebbe Elsborg

Thomas T. Hildebrandt

Henning Niss

Proceedings of the Foundations of Software Science and Computation Structures, 2006

Sortings for Reactive Systems.

[BibT_eX]

[DOI]

Søren Debois

Thomas T. Hildebrandt

Proceedings of the CONCUR 2006 - Concurrency Theory, 17th International Conference, 2006

Relational Reasoning for Recursive Types and References.

[BibT_eX]

[DOI]

Nina Bohr

Proceedings of the Programming Languages and Systems, 4th Asian Symposium, 2006

2005

Categorical models for Abadi and Plotkin's logic for parametricity.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2005

Synthetic Domain Theory and Models of Linear Abadi & Plotkin Logic.

[BibT_eX]

[DOI]

Giuseppe Rosolini

Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics, 2005

Parametric Domain-theoretic Models of Polymorphic Intuitionistic / Linear Lambda Calculus.

[BibT_eX]

[DOI]

Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics, 2005

Semantics of Separation-Logic Typing and Higher-Order Frame Rules.

[BibT_eX]

[DOI]

Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 2005

BI Hyperdoctrines and Higher-Order Separation Logic.

[BibT_eX]

[DOI]

Bodil Biering

Proceedings of the Programming Languages and Systems, 2005

2004

Preface: Recent Developments in Domain Theory: A collection of papers in honour of Dana S. Scott.

[BibT_eX]

[DOI]

Martín Hötzel Escardó

Achim Jung

Giuseppe Rosolini

Theor. Comput. Sci., 2004

Equilogical spaces.

[BibT_eX]

[DOI]

Andrej Bauer

Dana S. Scott

Theor. Comput. Sci., 2004

A Retrospective on Region-Based Memory Management.

[BibT_eX]

[DOI]

High. Order Symb. Comput., 2004

An infrastructure for context dependent mobile multimedia communication.

[BibT_eX]

[DOI]

J. Aa. Serensen

Kåre J. Kristoffersen

Proceedings of the IEEE 6th Workshop on Multimedia Signal Processing, 2004

2002

A general notion of realizability.

[BibT_eX]

[DOI]

Bull. Symb. Log., 2002

Relative and modified relative realizability.

[BibT_eX]

[DOI]

Jaap van Oosten

Ann. Pure Appl. Log., 2002

2001

A constraint-based region inference algorithm.

[BibT_eX]

[DOI]

Mads Tofte

Theor. Comput. Sci., 2001

2000

Developing Theories of Types and Computability via Realizability.

[BibT_eX]

[DOI]

Electronic Notes in Theoretical Computer Science 34, Elsevier, 2000

Continuous Functionals of Dependent Types and Equilogical Spaces.

[BibT_eX]

[DOI]

Andrej Bauer

Proceedings of the Computer Science Logic, 2000

Unification and polymorphism in region inference.

[BibT_eX]

Mads Tofte

Proceedings of the Proof, Language, and Interaction, Essays in Honour of Robin Milner, 2000

1999

Relational Interpretations of Recursive Types in an Operational Setting.

[BibT_eX]

[DOI]

Robert Harper

Inf. Comput., 1999

Preface.

[BibT_eX]

[DOI]

Proceedings of the Tutorial Workshop on Realizability Semantics and Applications, associated to FLoC'99, the 1999 Federated Logic Conference, Trento, Italy, June 30, 1999

Bibliography on Realizability.

[BibT_eX]

[DOI]

Proceedings of the Tutorial Workshop on Realizability Semantics and Applications, associated to FLoC'99, the 1999 Federated Logic Conference, Trento, Italy, June 30, 1999

Local Realizability Toposes and a Modal Logic for Computability.

[BibT_eX]

[DOI]

Steven Awodey

Dana S. Scott

Proceedings of the Tutorial Workshop on Realizability Semantics and Applications, associated to FLoC'99, the 1999 Federated Logic Conference, Trento, Italy, June 30, 1999

1998

A Region Inference Algorithm.

[BibT_eX]

[DOI]

Mads Tofte

ACM Trans. Program. Lang. Syst., 1998

On propositions-as-types in realizability models.

[BibT_eX]

[DOI]