Code-carrying theories

DOI10.1007/S00165-006-0013-4MaRDI QIDQ2643124zbMATH OpenOpenAlexFDO

Authors Bart Jacobs, Sjaak Smetsers, Ronny Wichers Schreur

Publication date 23 August 2007

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-006-0013-4

zbMATH Keywords

Code generationCompressionFunctional languagesProof assistantsPVSUnification

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Computer Aided Systems Theory – EUROCAST 2005
• scientific article; zbMATH DE number 4147469
• Program development by proof transformation.
• Proofs and programs: A naïve approach to program extraction
• Publication:5751976

Cites work

• A Machine-Oriented Logic Based on the Resolution Principle
• A universal algorithm for sequential data compression
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• scientific article; zbMATH DE number 2085164 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Program extraction from large proof developments
• Synthesis of ML programs in the system Coq
• Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
• Unification theory

Cited in

(2)

• Unified program generation and verification: a case study on number-theoretic transform
• Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving

Describes a project that uses

Uses Software

• Coq
• PVS
• JML
• PVSio
• Haskell
• ACL2
• CLEAN
• Isabelle/HOL

This page was built for publication: Code-carrying theories

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