Verifying higher-order programs with the dijkstra monad

No abstract is available for this paper.

• Publication year

  2013

• Venue

  ACM-SIGPLAN Symposium on Programming Language Design and Implementation

• Publication date

  2013-06-16

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/2491956.2491978
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Characteristic Formulae for the Veri cation of Imperative Programs

  2014cited by this paper
• Fully abstract compilation to JavaScript

  2013cited by this paper
• Nested refinements: a logic for duck typing

  2012cited by this paper
• Towards a program logic for JavaScript

  2012cited by this paper
• Verifying stateful programs with substructural state and hoare types

  2011cited by this paper
• Dependent types for JavaScript

  2011cited by this paper
• Lightweight monadic programming in ML

  2011cited by this paper
• Verified Security for Browser Extensions

  2011cited by this paper
• Characteristic formulae for the verification of imperative programs

  2011cited by this paper
• Secure distributed programming with value-dependent types

  2011cited by this paper
• Predicate abstraction and CEGAR for higher-order model checking

  2011cited by this paper
• Roles, stacks, histories: A triple for Hoare

  2010cited by this paper
• Type-preserving compilation of end-to-end verification of security enforcement

  2010cited by this paper
• CFA2: A Context-Free Approach to Control-Flow Analysis

  2010cited by this paper
• Semantic subtyping with an SMT solver

  2010cited by this paper
• Dafny: An Automatic Program Verifier for Functional Correctness

  2010cited by this paper
• A Polymorphic Intermediate Verification Language: Design and Logical Encoding

  2010cited by this paper
• The Essence of JavaScript

  2010influential reference
• Typechecking Higher-Order Security Libraries

  2010influential reference
• Logical types for untyped languages

  2010cited by this paper
• GATEKEEPER: Mostly Static Enforcement of Security and Reliability Policies for JavaScript Code

  2009influential reference
• Type Analysis for JavaScript

  2009cited by this paper
• Local Hoare reasoning about DOM

  2008cited by this paper
• Z3: An Efficient SMT Solver

  2008influential reference
• Liquid types

  2008cited by this paper
• JavaScript: The Good Parts

  2008cited by this paper
• Hoare type theory, polymorphism and separation1

  2008influential reference
• Ynot

  2008influential reference
• Abstract Predicates and Mutable ADTs in Hoare Type Theory

  2007influential reference
• The Why/Krakatoa/Caduceus Platform for Deductive Program Verification

  2007cited by this paper
• Separation logic and abstraction

  2005cited by this paper
• Soft typing

  2004cited by this paper
• Separation and information hiding

  2004cited by this paper
• Verification of Object-Oriented Programs with Invariants

  2003cited by this paper
• Safe Polymorphic Type Inference for Scheme: Translating Scheme to ML.

  1995cited by this paper
• Safe polymorphic type inference for a dynamically typed language: translating Scheme to ML

  1995cited by this paper
• Dynamic Typing: Syntax and Proof Theory

  1994cited by this paper
• A Practical Formal Semantic Definition and Verification System for TYPED LISP

  1976cited by this paper
• Guarded commands, nondeterminacy and formal derivation of programs

  1975influential reference
• Towards a Mathematical Science of Computation

  1962cited by this paper

• Foundational Multi-Modal Program Verifiers

  2026influential citation
• Close is Good Enough: Component-Based Synthesis Modulo Logical Similarity

  2025cites this paper
• coma, an Intermediate Verification Language with Explicit Abstraction Barriers

  2025cites this paper
• An interactive type checker for dependent types with general recursion (System Description)

  2025cites this paper
• Program Logics à la Carte

  2025cites this paper
• Formal Verification of Just-in-Time Compilation

  2025cites this paper
• A Denotational Product Construction for Temporal Verification of Effectful Higher-Order Programs

  2025cites this paper
• Abstract Interpretation of Temporal Safety Effects of Higher Order Programs

  2025cites this paper
• Thrust: A Prophecy-Based Refinement Type System for Rust

  2025cites this paper
• Type Inference Logics

  2024cites this paper
• Algebraic Effects Meet Hoare Logic in Cubical Agda

  2024cites this paper
• A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata

  2024cites this paper
• Succinct ordering and aggregation constraints in algebraic array theories

  2024cites this paper
• Verification Algorithms for Automated Separation Logic Verifiers

  2024cites this paper
• Security of AI Agents

  2024cites this paper
• Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification

  2024cites this paper
• Verifying Programs with Logic and Extended Proof Rules: Deep Embedding vs. Shallow Embedding

  2024cites this paper
• Securely Compiling F ★ Programs With IO and Then Linking Them Against Weakly-Typed Interfaces

  2023influential citation
• Higher-Order Weakest Precondition Transformers via a CPS Transformation

  2023cites this paper
• Cutting the Cake: A Language for Fair Division

  2023cites this paper
• On algebraic array theories

  2023cites this paper
• Dependently-Typed Programming with Logical Equality Reflection

  2023cites this paper
• Interaction Tree Specifications: A Framework for Specifying Recursive, Effectful Computations That Supports Auto-Active Verification (Artifact)

  2023cites this paper
• Morpheus: Automated Safety Verification of Data-dependent Parser Combinator Programs

  2023influential citation
• Formalizing, Verifying and Applying ISA Security Guarantees as Universal Contracts

  2023cites this paper
• Program adverbs and Tlön embeddings

  2022cites this paper
• Identifying Overly Restrictive Matching Paterns in SMT-based Program Verifiers (extended version)

  2022cites this paper
• An approach to translating Haskell programs to Agda and reasoning about them

  2022cites this paper
• CirC: Compiler infrastructure for proof systems, software verification, and more

  2022cites this paper
• Internship Proposal: Infinite Structures for Program Verification

  2022cites this paper
• Automatic Implementations Synthesis of Secure Protocols and Attacks from Abstract Models

  2022cites this paper
• Specification-guided component-based synthesis from effectful libraries

  2022cites this paper
• Verified symbolic execution with Kripke specification monads (and no meta-programming)

  2022cites this paper
• Proof Engineering with Predicate Transformer Semantics

  2022cites this paper
• Dijkstra monads forever: termination-sensitive specifications for interaction trees

  2021cites this paper
• The Multiverse: Logical Modularity for Proof Assistants

  2021cites this paper
• Steel: proof-oriented programming in a dependently typed concurrent separation logic

  2021cites this paper
• A General Semantic Construction of Dependent Refinement Type Systems, Categorically

  2021cites this paper
• Gillian, Part II: Real-World Verification for JavaScript and C

  2021cites this paper
• Programming and Proving with Indexed Effects

  2021cites this paper
• Identifying Overly Restrictive Matching Patterns in SMT-based Program Verifiers (Extended Version)

  2021cites this paper
• Refinements of Futures Past: Higher-Order Specification with Implicit Refinement Types (Extended Version)

  2021cites this paper
• How to safely use extensionality in Liquid Haskell

  2021cites this paper
• Modular specification and verification of closures in Rust

  2021cites this paper
• Reasoning about the garden of forking paths

  2021cites this paper
• Layered Indexed Effects: Foundations and Applications of Effectful Dependently Typed Programming

  2020influential citation
• Unifying graded and parameterised monads

  2020cites this paper
• Combining predicate transformer semantics for effects: a case study in parsing regular languages

  2020cites this paper
• ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs

  2020cites this paper
• Extending Liquid Types to Arrays

  2020cites this paper
• Higher-order demand-driven symbolic evaluation

  2020cites this paper
• Data-Flow Analyses as Effects and Graded Monads

  2020cites this paper
• Bayesian Optimisation of Solver Parameters in CBMC

  2020cites this paper
• A formalism to model higher-order function

  2020cites this paper
• General Semantic Construction of Dependent Refinement Type Systems, Categorically

  2020cites this paper
• Assisting End Users in Workflow Systems

  2020cites this paper
• A Framework for Resource Dependent EDSLs in a Dependently Typed Language (Artifact)

  2020cites this paper
• Numeric domains meet algebraic data types

  2020cites this paper
• Unifying Compilers for SNARKs, SMT, and More

  2020cites this paper
• Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms

  2019cites this paper
• The next 700 relational program logics

  2019cites this paper
• System FR: formalized foundations for the stainless verifier

  2019cites this paper
• A predicate transformer semantics for effects (functional pearl)

  2019cites this paper
• JaVerT 2.0: compositional symbolic execution for JavaScript

  2019cites this paper
• Mechanized Verification of the Correctness and Asymptotic Complexity of Programs. (Vérification mécanisée de la correction et complexité asymptotique de programmes)

  2019cites this paper
• A symbolic execution semantics for TopHat

  2019cites this paper
• Dijkstra monads for all

  2019influential citation
• Evolution , Semantics , and Engineering of the F ? Verification System May 19 , 2019

  2019cites this paper
• Experimental Evaluation of Formal Software Development Using Dependently Typed Languages

  2019influential citation
• Type system for resource bounds with type-preserving compilation

  2019cites this paper
• Algebraic effects, specification and refinement

  2019cites this paper
• QED at Large: A Survey of Engineering of Formally Verified Software

  2019cites this paper
• Behavioural Equivalence via Modalities for Algebraic Effects

  2018cites this paper
• The Formal Semantics and Evolution of the F ? Verification System October 11 , 2018

  2018cites this paper
• Secure, fast and verified cryptographic applications: a scalable approach. (Implémentations cryptographiques sures, performantes et verifiées: une approche passant a l'échelle)

  2018cites this paper
• Symbolic Execution for JavaScript

  2018cites this paper
• Meta-F⋆: Proof Automation with SMT, Tactics, and Metaprograms

  2018cites this paper
• Intrinsically-typed definitional interpreters for imperative languages

  2017cites this paper
• Local refinement typing

  2017cites this paper
• A Monadic Framework for Relational Verification (Functional Pearl)

  2017cites this paper
• TiML: a functional language for practical complexity analysis with invariants

  2017cites this paper
• A monadic framework for relational verification: applied to information security, program equivalence, and optimizations

  2017cites this paper
• Building Secure SGX Enclaves using F ∗ , C + + and X 64 Presentation Proposal for PRISC ’ 18

  2017cites this paper
• Recalling a witness: foundations and applications of monotonic state

  2017cites this paper
• JaVerT: JavaScript verification toolchain

  2017cites this paper
• Techniques for the verification of dynamically typed programs

  2017cites this paper
• Stateful manifest contracts

  2017cites this paper
• Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types

  2017cites this paper
• Hoare-style Reasoning with Higher-order Control: Continuations and Concurrency

  2017cites this paper
• A Coq Library for Internal Verification of Running-Times

  2016cites this paper
• DOM: Specification and Client Reasoning

  2016cites this paper
• Dependent types and multi-monadic effects in F*

  2016influential citation
• Semantic Foundations for F ?

  2016cites this paper
• Learning Program Specifications from Sample Runs

  2016cites this paper
• Dependent Types and Fibred Computational Effects

  2016cites this paper
• Dijkstra monads for free

  2016cites this paper
• C hainmail : Defensively Consistent Modular Specifications for an Open World

  2015cites this paper
• For Internal Verification of Running-Times

  2015cites this paper
• Bounded refinement types

  2015cites this paper
• Dijkstra and Hoare monads in monadic computation

  2015influential citation