On the public citation graph
Actris: session-type based reasoning in separation logic
0 signed · 89 inferred · view as graph
Inferred edges come from two machine sources: sweeps of open repository metadata (mostly SSRN and Zenodo), and a bulk OpenAlex citation snapshot. Every row below is labelled with the one it came from. Neither is a complete citation index — absence here is not evidence of absence.
Is this your work? Sign in with ORCID and put your name on the
claims that are yours.
Reference health. See whether every reference in this work resolves to a
known work and none has been retracted — and get a dated CiteStamped
badge you can embed.
What this work says
Outgoing claims: the papers this work cites, builds on, or argues with.
inferredcites →https://doi.org/10.1007/11817949_16openalex-snapshot
A New Type System for Deadlock-Free Processes
inferredcites →https://doi.org/10.1007/978-3-030-02768-1_16openalex-snapshot
Automated Modular Verification for Relaxed Communication Protocols
inferredcites →https://doi.org/10.1007/978-3-030-17184-1_22openalex-snapshot
Manifest Deadlock-Freedom for Shared Session Types
inferredcites →https://doi.org/10.1007/978-3-030-44914-8_13openalex-snapshot
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
inferredcites →https://doi.org/10.1007/978-3-319-30936-1_2openalex-snapshot
Conflation Confers Concurrency
inferredcites →https://doi.org/10.1007/978-3-642-10672-9_15openalex-snapshot
Proving Copyless Message Passing
inferredcites →https://doi.org/10.1007/978-3-642-14107-2_16openalex-snapshot
Type-Safe Eventful Sessions in Java
inferredcites →https://doi.org/10.1007/978-3-642-15375-4_12openalex-snapshot
A Theory of Design-by-Contract for Distributed Multiparty Interactions
inferredcites →https://doi.org/10.1007/978-3-642-24690-6_24openalex-snapshot
Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications
inferredcites →https://doi.org/10.1007/978-3-642-39038-8_13openalex-snapshot
Why Do Scala Developers Mix the Actor Model with other Concurrency Models?
inferredcites →https://doi.org/10.1007/978-3-642-54833-8_16openalex-snapshot
Communicating State Transition Systems for Fine-Grained Concurrent Resources
inferredcites →https://doi.org/10.1007/978-3-642-54833-8_9openalex-snapshot
Impredicative Concurrent Abstract Predicates
inferredcites →https://doi.org/10.1007/978-3-662-44202-9_9openalex-snapshot
TaDA: A Logic for Time and Data Abstraction
inferredcites →https://doi.org/10.1007/978-3-662-54434-1_26openalex-snapshot
The Essence of Higher-Order Concurrent Separation Logic
inferredcites →https://doi.org/10.1007/978-3-662-54434-1_34openalex-snapshot
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
inferredcites →https://doi.org/10.1007/bfb0053567openalex-snapshot
Language primitives and type discipline for structured communication-based programming
inferredcites →https://doi.org/10.1016/0022-0000(89)90027-5openalex-snapshot
Solving reflexive domain equations in a category of complete metric spaces
inferredcites →https://doi.org/10.1016/j.jlap.2003.07.006openalex-snapshot
The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML
inferredcites →https://doi.org/10.1016/j.scico.2018.08.005openalex-snapshot
Session-ocaml: A session-based library with polarities and lenses
inferredcites →https://doi.org/10.1017/cbo9781107256552openalex-snapshot
Program Logics for Certified Compilers
inferredcites →https://doi.org/10.1017/s0956796818000151openalex-snapshot
Iris from the ground up: A modular foundation for higher-order concurrent separation logic
inferredcites →https://doi.org/10.1109/iceccs.2015.33openalex-snapshot
Towards a Session Logic for Communication Protocols
inferredcites →https://doi.org/10.1145/1328438.1328472openalex-snapshot
Multiparty asynchronous session types
inferredcites →https://doi.org/10.1145/1328897.1328472openalex-snapshot
Multiparty asynchronous session types
inferredcites →https://doi.org/10.1145/1925844.1926417openalex-snapshot
Expressive modular fine-grained concurrency specification
inferredcites →https://doi.org/10.1145/2603088.2603116openalex-snapshot
Deadlock and lock freedom in the linear π-calculus
inferredcites →https://doi.org/10.1145/3093333.3009855openalex-snapshot
Interactive proofs in higher-order concurrent separation logic
inferredcites →https://doi.org/10.1145/3180155.3180157openalex-snapshot
A static verification framework for message passing in Go using behavioural types
inferredcites →https://doi.org/10.1145/3236772openalex-snapshot
MoSeL: a general, extensible modal framework for interactive proofs in separation logic
inferredcites →https://doi.org/10.1145/3297858.3304069openalex-snapshot
Understanding Real-World Concurrency Bugs in Go
inferredcites →https://doi.org/10.21276/ijre.2018.5.5.4openalex-snapshot
MapReduce: Simplified Data Processing on Large Cluster
inferredcites →https://doi.org/10.2168/lmcs-7(3:7)2011openalex-snapshot
Permission-Based Separation Logic for Message-Passing Concurrency
inferredcites →https://doi.org/10.2168/lmcs-8(4:1)2012openalex-snapshot
First steps in synthetic guarded domain theory: step-indexing in the topos of trees
inferredcites →https://doi.org/10.4204/eptcs.104.3openalex-snapshot
Shared Contract-Obedient Endpoints
inferredcites →https://doi.org/10.4204/eptcs.211.7openalex-snapshot
Future-based Static Analysis of Message Passing Programs
inferredcites →https://doi.org/10.4230/lipics.ecoop.2019.19openalex-snapshot
Transferring Obligations Through Synchronizations
What points at this work
Incoming claims: where this work appears in other papers’ reference lists and arguments.
inferred← citeshttps://doi.org/10.1007/978-3-030-44914-8_13openalex-snapshot
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
inferred← citeshttps://doi.org/10.1007/978-3-030-81685-8_17openalex-snapshot
Gobra: Modular Specification and Verification of Go Programs
inferred← citeshttps://doi.org/10.1007/978-3-030-99336-8_19openalex-snapshot
A Predicate Transformer for Choreographies
inferred← citeshttps://doi.org/10.1007/978-3-031-76554-4_12openalex-snapshot
VeyMont: Choreography-Based Generation of Correct Concurrent Programs with Shared Memory
inferred← citeshttps://doi.org/10.1007/978-3-031-91121-7_3openalex-snapshot
First-Person Choreographic Programming with Continuation-Passing Communications
inferred← citeshttps://doi.org/10.1007/978-3-031-95589-1openalex-snapshot
Coordination Models and Languages
inferred← citeshttps://doi.org/10.1007/978-3-032-05291-9_3openalex-snapshot
Actor Capabilities for Message Ordering
inferred← citeshttps://doi.org/10.1007/s10817-024-09701-wopenalex-snapshot
Refinement of Parallel Algorithms Down to LLVM: Applied to Practically Efficient Parallel Sorting
inferred← citeshttps://doi.org/10.1007/s10817-026-09765-wopenalex-snapshot
A Continuation-Based Solution of the Linearity Challenge
inferred← citeshttps://doi.org/10.1109/cgo51591.2021.9370317openalex-snapshot
GoBench: A Benchmark Suite of Real-World Go Concurrency Bugs
inferred← citeshttps://doi.org/10.1109/conisoft50191.2020.00024openalex-snapshot
Formal Verification of a Database Management System
inferred← citeshttps://doi.org/10.1134/s036176882108017xopenalex-snapshot
Database Management System Verification with Separation Logics
inferred← citeshttps://doi.org/10.1145/3409003openalex-snapshot
SteelCore: an extensible concurrent separation logic for effectful dependently typed programs
inferred← citeshttps://doi.org/10.1145/3428216openalex-snapshot
Statically verified refinements for multiparty protocols
inferred← citeshttps://doi.org/10.1145/3434286openalex-snapshot
On algebraic abstractions for concurrent separation logics
inferred← citeshttps://doi.org/10.1145/3434314openalex-snapshot
A separation logic for effect handlers
inferred← citeshttps://doi.org/10.1145/3453483.3454041openalex-snapshot
Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes
inferred← citeshttps://doi.org/10.1145/3473590openalex-snapshot
Steel: proof-oriented programming in a dependently typed concurrent separation logic
inferred← citeshttps://doi.org/10.1145/3498662openalex-snapshot
Connectivity graphs: a method for proving deadlock freedom based on separation logic
inferred← citeshttps://doi.org/10.1145/3547631openalex-snapshot
Later credits: resourceful reasoning for the later modality
inferred← citeshttps://doi.org/10.1145/3607856openalex-snapshot
Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)
inferred← citeshttps://doi.org/10.1145/3607859openalex-snapshot
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols
inferred← citeshttps://doi.org/10.1145/3632889openalex-snapshot
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
inferred← citeshttps://doi.org/10.1145/3689732openalex-snapshot
Verified Lock-Free Session Channels with Linking
inferred← citeshttps://doi.org/10.1145/3689762openalex-snapshot
Multris: Functional Verification of Multiparty Message Passing in Separation Logic
inferred← citeshttps://doi.org/10.1145/3720493openalex-snapshot
Characterizing Implementability of Global Protocols with Infinite States and Data
inferred← citeshttps://doi.org/10.1145/3756907.3756909openalex-snapshot
Mechanized Type Soundness for Substructural Types using Iris
inferred← citeshttps://doi.org/10.1145/3776730openalex-snapshot
Cryptis: Cryptographic Reasoning in Separation Logic
inferred← citeshttps://doi.org/10.1145/3779031.3779095openalex-snapshot
Building Blocks for Step-Indexed Program Logics
inferred← citeshttps://doi.org/10.1145/3808319openalex-snapshot
Implementability of Global Distributed Protocols Modulo Network Architectures
inferred← citeshttps://doi.org/10.1145/3815176openalex-snapshot
Formalising Asynchronous Session Subtyping
inferred← citeshttps://doi.org/10.1145/3828682openalex-snapshot
Completeness of Iris-Based Program Logics
inferred← citeshttps://doi.org/10.26226/morressier.604907f41a80aac83ca25d44openalex-snapshot
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
inferred← citeshttps://doi.org/10.3390/app10113928openalex-snapshot
An Abstraction Technique for Verifying Shared-Memory Concurrency
inferred← citeshttps://doi.org/10.3929/ethz-b-000489119openalex-snapshot
Gobra: Modular Specification and Verification of Go Programs (extended version)
inferred← citeshttps://doi.org/10.46298/entics.12286openalex-snapshot
Dependent Type Refinements for Futures
inferred← citeshttps://doi.org/10.46298/lmcs-17(3:9)2021openalex-snapshot
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
inferred← citeshttps://doi.org/10.46298/lmcs-18(2:16)2022openalex-snapshot
Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic
inferred← citeshttps://doi.org/10.48550/arxiv.2007.13685openalex-snapshot
Extending Concurrent Separation Logic to Enhance Modular Formalization
inferred← citeshttps://doi.org/10.48550/arxiv.2103.10269openalex-snapshot
Zooid: a DSL for Certified Multiparty Computation
inferred← citeshttps://doi.org/10.70675/95fceee8z06bbz48ccz8b06z87fb9e672ea8openalex-snapshot
Proof-oriented domain-specific language design for high-assurance software
Editorial review for independent work. ICSAC — the Institute for Complexity
Science and Advanced Computing — runs a structured editorial panel for researchers
publishing outside journals, and publishes on CiteStamp rails. Submission is free
and goes through ORCID: icsacinstitute.org/submit.