Mechanizing coinduction and corecursion in higher-order logic

DOI10.1093/LOGCOM/7.2.175MaRDI QIDQ4340418zbMATH OpenOpenAlexFDO

Authors Lawrence C. Paulson

Publication date 14 December 1997

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://www.repository.cam.ac.uk/handle/1810/276436

zbMATH Keywords

higher-order logicIsabelle

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Foundational (co)datatypes and (co)recursion for higher-order logic
• scientific article; zbMATH DE number 1424015
• A fixedpoint approach to implementing (co)inductive definitions
• Set theory for verification. II: Induction and recursion

Cited in

(24)

• HasCasl: integrated higher-order specification and program development
• Universal coalgebra: A theory of systems
• Foundational (co)datatypes and (co)recursion for higher-order logic
• Set theory for verification. II: Induction and recursion
• Embedding and automating conditional logics in classical higher-order logic
• Cut elimination for a logic with induction and co-induction
• On the key dependent message security of the Fujisaki-Okamoto constructions
• Inductive and coinductive components of corecursive functions in Coq
• Truly modular (co)datatypes for Isabelle/HOL
• Foundational extensible corecursion: a proof assistant perspective
• Friends with benefits. Implementing corecursion in foundational proof assistants
• scientific article; zbMATH DE number 2185691 (Why is no real title available?)
• scientific article; zbMATH DE number 7037626 (Why is no real title available?)
• A Purely Definitional Universal Domain
• Invited Talk: Coherentisation of First-Order Logic
• Using Structural Recursion for Corecursion
• scientific article; zbMATH DE number 1424015 (Why is no real title available?)
• scientific article; zbMATH DE number 7407797 (Why is no real title available?)
• Mechanical Reasoning about Families of UTP Theories
• Practical coinduction
• Automating Coherent Logic
• The optimal fixed point combinator
• Formalising Mathematics in Simple Type Theory
• Squeezing streams and composition of self-stabilizing algorithms

Describes a project that uses

Uses Software

• Isabelle
• TPS
• Isabelle/ZF

This page was built for publication: Mechanizing coinduction and corecursion in higher-order logic

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