Moessner's theorem: an exercise in coinductive reasoning in \textsc{Coq}

DOI10.1007/978-3-319-30734-3_21zbMath1475.68456OpenAlexW2418306939MaRDI QIDQ2026804

Louis Parlant, Alexandra Silva, Robbert Krebbers

Publication date: 20 May 2021

Full work available at URL: https://doi.org/10.1007/978-3-319-30734-3_21

Mathematics Subject Classification ID

Special sequences and polynomials (11B83) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (1)

Formalizing Moessner's theorem and generalizations in \textsc{Nuprl}

Uses Software

• Coq

This page was built for publication: Moessner's theorem: an exercise in coinductive reasoning in \textsc{Coq}