Email Gateway (Aug 18 2022 at 15:45): Email Gateway (Aug 18 2022 at 15:45):From: Christian Urban <urbanc@in.tum.de>
Dear Yongjian,
Who could introduce more technical papers on the relation between the two
features.
I think two good starting pointers to the
(Isabelle-centric) literature on this
topic are
Inductive datatypes in HOL - lessons learned in
Formal-Logic Engineering.
by Stefan Berghofer and Markus Wenzel
http://www4.in.tum.de/~berghofe/papers/TPHOLs99.pdf
and
A fixedpoint approach to (co)inductive and (co)datatype definitions
by Larry Paulson
http://www.cl.cam.ac.uk/~lp15/papers/Sets/milner-ind-defs.pdf
However, I assume there are experts on this
mailing list, which can give more detailed
answers.
Best wishes,
Christian
Last updated: Apr 19 2024 at 20:15 UTC