On a machine-checked proof for fraction arithmetic over a GCD domain

DOI10.1134/S0361768820020073zbMath1455.68249OpenAlexW3016698841MaRDI QIDQ2217198

S. D. Meshveliani

Publication date: 18 December 2020

Published in: Programming and Computer Software (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1134/s0361768820020073

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to number theory (11-04) Computational number theory (11Y99) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

DoCon-A

Uses Software

• AXIOM
• Coq
• Haskell
• Agda
• Lean

Cites Work

• Combinatory logic. With two sections by William Craig.
• The Lean Theorem Prover (System Description)
• Dependently Typed Programming in Agda
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On a machine-checked proof for fraction arithmetic over a GCD domain