Mechanizing coinduction and corecursion in higher-order logic
From MaRDI portal
Publication:4340418
DOI10.1093/logcom/7.2.175zbMath0878.68111OpenAlexW2053068669MaRDI QIDQ4340418
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
Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)
Related Items (11)
A Purely Definitional Universal Domain ⋮ Formalising Mathematics in Simple Type Theory ⋮ Practical coinduction ⋮ Squeezing streams and composition of self-stabilizing algorithms ⋮ Cut elimination for a logic with induction and co-induction ⋮ Friends with Benefits ⋮ On the Key Dependent Message Security of the Fujisaki-Okamoto Constructions ⋮ HasCasl: integrated higher-order specification and program development ⋮ Using Structural Recursion for Corecursion ⋮ Universal coalgebra: A theory of systems ⋮ Inductive and Coinductive Components of Corecursive Functions in Coq
Uses Software
This page was built for publication: Mechanizing coinduction and corecursion in higher-order logic
