On the public citation graph
Omnisemantics: Smooth Handling of Nondeterminism
0 signed · 60 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.1006/inco.1994.1093openalex-snapshot
A Syntactic Approach to Type Soundness
inferredcites →https://doi.org/10.1006/inco.1995.1134openalex-snapshot
Forward and Backward Simulations
inferredcites →https://doi.org/10.1007/3-540-44802-0_1openalex-snapshot
Local Reasoning about Programs that Alter Data Structures
inferredcites →https://doi.org/10.1007/978-3-030-17184-1_1openalex-snapshot
Time Credits and Time Receipts in Iris
inferredcites →https://doi.org/10.1007/978-3-642-37036-6_3openalex-snapshot
Pretty-Big-Step Semantics
inferredcites →https://doi.org/10.1007/978-3-642-39634-2_25openalex-snapshot
Handcrafted Inversions Made Operational on Operational Semantics
inferredcites →https://doi.org/10.1007/978-3-642-39799-8_34openalex-snapshot
Probabilistic Program Analysis with Martingales
inferredcites →https://doi.org/10.1007/978-3-662-49498-1_15openalex-snapshot
Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
inferredcites →https://doi.org/10.1007/978-3-662-49498-1_28openalex-snapshot
Transfinite Step-Indexing: Decoupling Concrete and Logical Steps
inferredcites →https://doi.org/10.1007/978-3-662-54434-1_22openalex-snapshot
Verified Characteristic Formulae for CakeML
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/b138392openalex-snapshot
Abstraction, Refinement and Proof for Probabilistic Systems
inferredcites →https://doi.org/10.1007/s10817-009-9148-3openalex-snapshot
Mechanized Semantics for the Clight Subset of the C Language
inferredcites →https://doi.org/10.1007/s10817-009-9155-4openalex-snapshot
A Formally Verified Compiler Back-end
inferredcites →https://doi.org/10.1007/s10817-017-9431-7openalex-snapshot
Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits
inferredcites →https://doi.org/10.1016/0022-0000(79)90006-0openalex-snapshot
Semantics of nondeterminism, concurrency, and communication
inferredcites →https://doi.org/10.1016/0304-3975(83)90055-5openalex-snapshot
A continuous semantics for unbounded nondeterminism
inferredcites →https://doi.org/10.1016/b978-0-7204-2233-7.50001-0openalex-snapshot
STUDIES IN LOGIC AND THE FOUNDATIONS OF MATHEMATICS
inferredcites →https://doi.org/10.1016/j.entcs.2019.09.016openalex-snapshot
A Denotational Semantics for Low-Level Probabilistic Programs with Nondeterminism
inferredcites →https://doi.org/10.1016/j.ic.2007.12.004openalex-snapshot
Coinductive big-step operational semantics
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/lics.2002.1029817openalex-snapshot
Separation logic: a logic for shared mutable data structures
inferredcites →https://doi.org/10.1109/lics.2005.47openalex-snapshot
Semantics of Separation-Logic Typing and Higher-Order Frame Rules
inferredcites →https://doi.org/10.1145/1708016.1708025openalex-snapshot
Verifying event-driven programs using ramified frame properties
inferredcites →https://doi.org/10.1145/2398856.2364546openalex-snapshot
Operational semantics using the partiality monad
inferredcites →https://doi.org/10.1145/2429069.2429131openalex-snapshot
The ramifications of sharing in data structures
inferredcites →https://doi.org/10.1145/2500365.2500592openalex-snapshot
The bedrock structured programming system
inferredcites →https://doi.org/10.1145/2660193.2660201openalex-snapshot
Compiler verification meets cross-language linking via data abstraction
inferredcites →https://doi.org/10.1145/2854065.2854083openalex-snapshot
Axiomatic semantics for compiler verification
inferredcites →https://doi.org/10.1145/2933575.2935313openalex-snapshot
Semantics for probabilistic programming
inferredcites →https://doi.org/10.1145/2983990.2984008openalex-snapshot
Type soundness for dependent object types (DOT)
inferredcites →https://doi.org/10.1145/3158121openalex-snapshot
A new proof rule for almost-sure termination
inferredcites →https://doi.org/10.1145/3290347openalex-snapshot
Quantitative separation logic: a logic for reasoning about probabilistic pointer programs
inferredcites →https://doi.org/10.1145/3371119openalex-snapshot
Interaction trees: representing recursive and impure programs in Coq
inferredcites →https://doi.org/10.1145/3408998openalex-snapshot
Separation logic for sequential programs (functional pearl)
inferredcites →https://doi.org/10.1145/3460860openalex-snapshot
An Extended Account of Trace-relating Compiler Correctness and Secure Compilation
inferredcites →https://doi.org/10.1145/6490.6494openalex-snapshot
Countable nondeterminism and random assignment
inferredcites →https://doi.org/10.1145/99583openalex-snapshot
Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '91
inferredcites →https://doi.org/10.2168/lmcs-9(4:4)2013openalex-snapshot
Step-Indexed Relational Reasoning for Countable Nondeterminism
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-032-12086-1_4openalex-snapshot
A Research Agenda for the Living SysML V2 Blueprint: Toward Executable, Verifiable, and Navigable System Models
inferred← citeshttps://doi.org/10.1145/3656439openalex-snapshot
Live Verification in an Interactive Proof Assistant
inferred← citeshttps://doi.org/10.1145/3656446openalex-snapshot
Foundational Integration Verification of a Cryptographic Server
inferred← citeshttps://doi.org/10.1145/3703595.3705890openalex-snapshot
Monadic Interpreters for Concurrent Memory Models
inferred← citeshttps://doi.org/10.1145/3729318openalex-snapshot
Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
inferred← citeshttps://doi.org/10.1145/3747509openalex-snapshot
Formal Semantics and Program Logics for a Fragment of OCaml
inferred← citeshttps://doi.org/10.1145/3756681.3757034openalex-snapshot
QADL: Prototype of Quantum Architecture Description Language
inferred← citeshttps://doi.org/10.1145/3756907.3756926openalex-snapshot
Abstract machines and small-step semantics: a winning ticket for proof automation?
inferred← citeshttps://doi.org/10.1145/3759425.3763391openalex-snapshot
A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
inferred← citeshttps://doi.org/10.1145/3779031.3779088openalex-snapshot
Foundational Verification of Running-Time Bounds for Interactive Programs
inferred← citeshttps://doi.org/10.1145/3797874openalex-snapshot
Denotation-based Compositional Compiler Verification
inferred← citeshttps://doi.org/10.1145/3798260openalex-snapshot
Mechanised Semantics of Multi-stage Programming
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.