Programming Languages and Systems
From MaRDI portal
Publication:5308710
DOI10.1007/b96702zbMath1126.68475OpenAlexW2964738244MaRDI QIDQ5308710
Jean-Christophe Filliâtre, Pierre Letouzey
Publication date: 28 September 2007
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/b96702
Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)
Related Items (12)
Trace-based verification of imperative programs with I/O ⋮ Extracting functional programs from Coq, in Coq ⋮ Extraction in Coq: An Overview ⋮ Efficient extensional binary tries ⋮ Unnamed Item ⋮ A case study in formalizing projective geometry in Coq: Desargues theorem ⋮ An assertional proof of red-black trees using Dafny ⋮ Building Certified Static Analysers by Modular Construction of Well-founded Lattices ⋮ A Coq Library for Internal Verification of Running-Times ⋮ Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism ⋮ Automatic Functional Correctness Proofs for Functional Search Trees ⋮ Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code
Uses Software
This page was built for publication: Programming Languages and Systems
