A two-level approach towards lean proof-checking

DOI10.1007/3-540-61780-9_59zbMATH Open1407.68431OpenAlexW1500329306MaRDI QIDQ4647567FDOQ4647567

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Exploring abstract algebra in constructive type theory
• A two-level approach towards lean proof-checking

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

Uses Software

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

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)