scientific article; zbMATH DE number 1980941

MaRDI QIDQ4428316zbMATH OpenFDO

Authors Don Syme, Andrew D. Gordon

Publication date 15 September 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2514/25140418.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 1614692
• Automated proof construction in type theory using resolution
• Type soundness proofs with definitional interpreters
• scientific article; zbMATH DE number 1552510
• On automating the extraction of programs from proofs using product types
• Dependently Typed Programming Based on Automated Theorem Proving
• Automating soundness proofs
• Modular and automated type-soundness verification for language extensions
• A type reduction from proof-conditional to dynamic semantics
• Parameterized recursive refinement types for automated program verification

Cited in

(3)

• Automating soundness proofs
• Modular and automated type-soundness verification for language extensions
• Tool-assisted specification and verification of typed low-level languages

Describes a project that uses

Uses Software

• OCaml

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4428316)