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

DOI10.1007/978-3-319-30734-3_21MaRDI QIDQ2026804zbMATH OpenOpenAlexFDO

Authors Robbert Krebbers, Louis Parlant, Alexandra Silva

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)

Recommendations

• A proof of Moessner's theorem by coinduction
• On Moessner's theorem
• A characterization of Moessner's sieve
• Incremental pattern-based coinduction for process algebra and its Isabelle formalization
• Moessnerian theorems. How to prove them by simple graph theoretical inspection

Cited in

(6)

• A proof of Moessner's theorem by coinduction
• Mac Lane's comparison theorem for the Kleisli construction formalized in Coq
• A characterization of Moessner's sieve
• Formalizing Moessner's theorem and generalizations in \textsc{Nuprl}
• Shall we juggle, coinductively?
• scientific article; zbMATH DE number 7566073 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

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

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