A two-level approach towards lean proof-checking

DOI10.1007/3-540-61780-9_59zbMath1407.68431OpenAlexW1500329306MaRDI QIDQ4647567

Gilles Barthe, Mark Ruys, Hendrik Pieter 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

computer algebra systemtype theoryuniversal algebraequational theoryequational problem

Mathematics Subject Classification ID

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

Related Items (4)

A two-level approach towards lean proof-checking ⋮ An Interactive Driver for Goal-directed Proof Strategies ⋮ Proof by computation in the Coq system ⋮ Formal Proofs for Nonlinear Optimization

Uses Software

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

Cites Work

• A two-level approach towards lean proof-checking
• Exploring abstract algebra in constructive type theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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