A fixedpoint approach to implementing (Co)inductive definitions

DOI10.1007/3-540-58156-1_11zbMath1433.68560OpenAlexW1485127463MaRDI QIDQ5210768

Lawrence Charles Paulson

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58156-1_11

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (12)

A general mathematics of names ⋮ I/O automata in Isabelle/HOL ⋮ A concrete final coalgebra theorem for ZF set theory ⋮ Friends with Benefits ⋮ An embedding of Ruby in Isabelle ⋮ A higher-order interpretation of deductive tableau ⋮ On the Key Dependent Message Security of the Fujisaki-Okamoto Constructions ⋮ Using a generalisation critic to find bisimulations for coinductive proofs ⋮ NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF ⋮ Program development schemata as derived rules ⋮ Coalgebras as Types Determined by Their Elimination Rules ⋮ Structuring metatheory on inductive definitions

Uses Software

• Isabelle/ZF
• IMPS
• EVES
• Cambridge LCF

Cites Work

• A co-induction principle for recursively defined domains
• Set theory for verification. I: From foundations to functions
• IMPS: An interactive mathematical proof system
• Set theory for verification. II: Induction and recursion
• Logic and Computation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A fixedpoint approach to implementing (Co)inductive definitions