Programming and computing in HOL

DOI10.1007/3-540-44659-1_2MaRDI QIDQ2754029zbMATH OpenFDO

Authors Bruno Barras

Publication date 11 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44659-1_2

Mathematics Subject Classification ID

Recommendations

• A few exercises in theorem processing
• scientific article; zbMATH DE number 234014
• scientific article; zbMATH DE number 2185700
• HOL Light: An Overview
• Interpreting HOL in the calculus of constructions

Cited in

(13)

• Verification of the Miller-Rabin probabilistic primality test.
• Interpreting HOL in the calculus of constructions
• Flyspeck II: The basic linear programs
• Rewriting conversions implemented with continuations
• scientific article; zbMATH DE number 2185700 (Why is no real title available?)
• Validating QBF Validity in HOL4
• A Brief Overview of HOL4
• A Compiled Implementation of Normalization by Evaluation
• A Thread of HOL Development
• scientific article; zbMATH DE number 1163076 (Why is no real title available?)
• Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
• Fast, verified computation for HOL ITPs
• A few exercises in theorem processing

Describes a project that uses

Uses Software

• HOL

This page was built for publication: Programming and computing in HOL

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