Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [Agda] [Coq-Club] Prior work on proof assistan...

Email Gateway (Aug 23 2022 at 09:08):

From: Wolfram Kahl <kahl@cas.mcmaster.ca>
So technically, the lost sharing is the second-order sharing that is preserved
in ``optimal reduction'' of lambda calculi [Levy-1980, Lamping-1990, Asperti-Laneve-1992],
while hash consing normally is directly usable only for first-order sharing.

Wolfram

Last updated: Apr 23 2024 at 12:29 UTC