A two-level approach towards lean proof-checking

DOI10.1007/3-540-61780-9_59MaRDI QIDQ4647567zbMATH OpenOpenAlexFDO

Authors Gilles Barthe, Mark Ruys, Henk Barendregt

Publication date 15 January 2019

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

Full work available at URL http://hdl.handle.net/2066/17271

zbMATH Keywords

type theoryuniversal algebraequational theorycomputer algebra systemequational problem

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 4009856
• Proof certificates for equality reasoning
• Proof search and proof check for equational and inductive theorems.
• The Proof Certifier Checkers
• Interactive proof-search for equational reasoning

Cites work

• scientific article; zbMATH DE number 3720983 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 1254246 (Why is no real title available?)
• scientific article; zbMATH DE number 1302061 (Why is no real title available?)
• scientific article; zbMATH DE number 591911 (Why is no real title available?)
• A two-level approach towards lean proof-checking
• Exploring abstract algebra in constructive type theory

Cited in

(6)

• Formal Proofs for Nonlinear Optimization
• Congruence types
• Formalising the Kruskal-Katona theorem in Lean
• A two-level approach towards lean proof-checking
• Proof by computation in the Coq system
• An Interactive Driver for Goal-directed Proof Strategies

Describes a project that uses

Uses Software

• LEGO
• ALF
• Automath
• Nuprl
• HOL
• Maple
• Isabelle
• Coq

This page was built for publication: A two-level approach towards lean proof-checking

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