5 citations · 9 across the 2 of their papers we have counts for
2 papers
cs.LO2018★ 4 cited
Design and Implementation of the Andromeda Proof Assistant
Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter +2
Andromeda is an LCF-style proof assistant where the user builds derivable judgments by writing code in a meta-level programming language AML. The only trusted component of Andromed…
cs.LO2016★ 5 cited
Formalising Real Numbers in Homotopy Type Theory
Gaëtan Gilbert
Cauchy reals can be defined as a quotient of Cauchy sequences of rationals. The limit of a Cauchy sequence of Cauchy reals is defined through lifting it to a sequence of Cauchy seq…