Who: a verifier for effectful higher-order programs

No abstract is available for this paper.

• Publication year

  2009

• Venue

  Proceedings of the 2009 ACM SIGPLAN workshop on ML

• Publication date

  2009-08-30

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/1596627.1596634
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Ynot : Reasoning with the Awkward Squad

  2008cited by this paper
• A Hoare Logic for Call-by-Value Functional Programs

  2008cited by this paper
• Ynot

  2008cited by this paper
• Formal Methods for Components and Objects

  2008cited by this paper
• Functional translation of a calculus of capabilities

  2008influential reference
• Proceedings of the 19th international conference on Computer aided verification

  2007cited by this paper
• Typing termination in a higher-order concurrent imperative language

  2007cited by this paper
• The Why/Krakatoa/Caduceus Platform for Deductive Program Verification

  2007cited by this paper
• Boogie: A Modular Reusable Verifier for Object-Oriented Programs

  2005cited by this paper
• An observationally complete program logic for imperative higher-order functions

  2005cited by this paper
• A logical analysis of aliasing in imperative higher-order functions

  2005cited by this paper
• The Spec# Programming System: An Overview

  2004cited by this paper
• Producing all ideals of a forest, functionally

  2003cited by this paper
• Verification of non-functional programs using interpretations in type theory

  2003influential reference
• From Algol to polymorphic linear lambda-calculus

  2000cited by this paper
• Region-based Memory Management

  1997cited by this paper
• A Gray Code for the Ideals of a Forest Poset

  1993cited by this paper
• The art of computer programming

  1983cited by this paper
• The Mechanical Evaluation of Expressions

  1964cited by this paper

• A Framework for the Automated Verification of Algebraic Effects and Handlers (extended version)

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

  2021cites this paper
• A Deductive Verification Framework For Higher Order Programs

  2020cites this paper
• Desfuncionalizar para Provar

  2019cites this paper
• Practical Methods for Reasoning About Java 8's Functional Programming Features

  2018cites this paper
• Défonctionnaliser pour prouver

  2016cites this paper
• Characteristic Formulae for the Veri cation of Imperative Programs

  2014cites this paper
• Automating Theorem Proving with SMT

  2013cites this paper
• BSP-Why, un outil pour la vérification déductive de programmes BSP : machine-checked semantics and application to distributed state-space algorithms. (BSP-Why, a tool for deductive verification of BSP programs : sémantiques mécanisées et application aux algorithmes d'espace d'états distribués)

  2013cites this paper
• Verification Condition Generation with the Dijkstra State Monad

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

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

  2011cites this paper
• Reverse Hoare Logic

  2011cites this paper
• Specifying generic Java programs: two case studies

  2010cites this paper
• Specifying Imperative ML-Like Programs Using Dynamic Logic

  2010cites this paper
• BSP-WHY: an intermediate language for deductive verification of BSP programs

  2010cites this paper
• Program verification through characteristic formulae

  2010cites this paper
• Reasoning about Function Objects

  2010cites this paper
• Program verification through characteristic formulae

  2010cites this paper