Code-carrying theories

DOI10.1007/s00165-006-0013-4zbMath1121.68030OpenAlexW2158209653MaRDI QIDQ2643124

Ronny Wichers Schreur, Bart Jacobs, Sjaak Smetsers

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

PVSUnificationCompressionCode generationFunctional languagesProof assistants

Mathematics Subject Classification ID

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

Related Items (1)

Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Synthesis of ML programs in the system Coq
• Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
• Program Extraction from Large Proof Developments
• A universal algorithm for sequential data compression
• Formal certification of a compiler back-end or
• A Machine-Oriented Logic Based on the Resolution Principle

This page was built for publication: Code-carrying theories