Pages that link to "Item:Q5410698"

The following pages link to Impredicative Concurrent Abstract Predicates (Q5410698):

Displaying 30 items.

• Abstract local reasoning for concurrent libraries: mind the gap (Q283756) (← links)
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) (Q832157) (← links)
• Balancing expressiveness in formal approaches to concurrency (Q890478) (← links)
• A perspective on specifying and verifying concurrent modules (Q1648035) (← links)
• Formally verifying exceptions for low-level code with separation logic (Q1683698) (← links)
• Lewis meets Brouwer: constructive strict implication (Q1688950) (← links)
• A model of guarded recursion via generalised equilogical spaces (Q1704599) (← links)
• On models of higher-order separation logic (Q2130583) (← links)
• Higher-order linearisability (Q2423744) (← links)
• Modular Termination Verification for Non-blocking Concurrency (Q2802477) (← links)
• Transfinite Step-Indexing: Decoupling Concrete and Logical Steps (Q2802498) (← links)
• Guarded Dependent Type Theory with Coinductive Types (Q2811330) (← links)
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types (Q2974778) (← links)
• A Light Modality for Recursion (Q2988388) (← links)
• Caper (Q2988651) (← links)
• The Essence of Higher-Order Concurrent Separation Logic (Q2988664) (← links)
• A Higher-Order Logic for Concurrent Termination-Preserving Refinement (Q2988673) (← links)
• Abstract Specifications for Concurrent Maps (Q2988678) (← links)
• Verifying Concurrent Graph Algorithms (Q3179300) (← links)
• Denotational semantics of recursive types in synthetic guarded domain theory (Q4623133) (← links)
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic (Q4625160) (← links)
• Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems (Q5041100) (← links)
• (Q5094146) (← links)
• (Q5111648) (← links)
• Denotational semantics for guarded dependent type theory (Q5139284) (← links)
• (Q5155670) (← links)
• Steps in modular specifications for concurrent modules (invited tutorial paper) (Q5971389) (← links)
• A model of PCF in guarded type theory (Q5971407) (← links)
• Is Impredicativity Implicitly Implicit (Q6079240) (← links)
• Concise outlines for a complex logic: a proof outline checker for TaDA (Q6145023) (← links)