Types for Proofs and Programs

DOI10.1007/11617990MaRDI QIDQ5897606zbMATH OpenOpenAlexFDO

Authors Lionel Elie Mamane

Publication date 13 November 2006

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

Full work available at URL https://doi.org/10.1007/11617990

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Nonstandard arithmetic (number-theoretic aspects) (11U10)

Recommendations

• scientific article; zbMATH DE number 3957253
• scientific article; zbMATH DE number 1696612
• An algebraic (set) theory of surreal numbers. I
• A simple canonical representation of rational numbers
• scientific article; zbMATH DE number 1088050

Cited in

(10)

• A framework for defining logical frameworks
• A simple canonical representation of rational numbers
• Licensing the Mizar Mathematical Library (MML)
• Conway numbers -- formal introduction
• The ring of Conway numbers in Mizar
• Conway's normal form in the Mizar system
• Surreal dyadic and real numbers: a formal construction
• Surreal numbers: a study of square roots
• Conway normal form: bridging approaches for comprehensive formalization of surreal numbers
• Inverse element for surreal number

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Types for Proofs and Programs

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