Verification of non-functional programs using interpretations in type theory
From MaRDI portal
Publication:4461768
DOI10.1017/S095679680200446XzbMath1111.68389MaRDI QIDQ4461768
Publication date: 18 May 2004
Published in: Journal of Functional Programming (Search for Journal in Brave)
Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (12)
The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML ⋮ Generalized arrays for Stainless frames ⋮ Modular inference of subprogram contracts for safety checking ⋮ Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language ⋮ Function extraction ⋮ Proofs of randomized algorithms in Coq ⋮ Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves ⋮ Inferring Loop Invariants Using Postconditions ⋮ Transforming Programs into Recursive Functions ⋮ Typing termination in a higher-order concurrent imperative language ⋮ Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory ⋮ Adapting functional programs to higher order logic
Uses Software
This page was built for publication: Verification of non-functional programs using interpretations in type theory
