Embedded domain specific verifiers

DOI10.1007/978-3-031-22337-2_26zbMath1528.68227OpenAlexW4313043206MaRDI QIDQ6113993

Ranjit Jhala

Publication date: 10 August 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-031-22337-2_26

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Refinement for structured concurrent programs
• Refinement types for Haskell
• Bounded refinement types
• Refinement Types for Ruby
• Simplify: a theorem prover for program checking
• Guarded commands, nondeterminacy and formal derivation of programs
• Low-level liquid types
• LMS-Verify: abstraction without regret for verified systems programming
• An axiomatic basis for computer programming

This page was built for publication: Embedded domain specific verifiers