Email Gateway (Aug 18 2022 at 10:58): Email Gateway (Aug 18 2022 at 10:58):From: Marco Maggesi <maggesi@math.unifi.it>
Moez A. Abdel-Gawad wrote:
Hi Moez,
in this paper
André Hirschowitz, Marco Maggesi
"Modules over Monads and Linearity"
Leivant, Queiroz (Eds.). WoLLIC 2007. LNCS 4576
we advocate the use of "linear morphism" as the good way to capture the
notion of "compatibility with substitution".
We have two Coq formalizations which adopt this discipline.
The first one is about Lambda Calculus:
http://web.math.unifi.it/~maggesi/mechanized/lambda/
(an equivalent translation in HOL-Light is also available from the same
page).
The other is about Fsub (part 1A of the poplmark challenge, to be precise):
http://web.math.unifi.it/~maggesi/mechanized/fsub/
The latter is especially compact and short (according to our own
statistics) compared to other proposed approach and does not require any
specific framework or library.
M.
Last updated: Nov 21 2024 at 12:39 UTC