Ken,
You should know about the Edinburgh Logical Framework (ELF), best
implemented in the Twelf system. While ELF is a particular framework, there
is tons of work about specification and programming in dependently typed
frameworks. See e.g. many papers by Frank Pfenning, Amy Felty, Bob Harper,
Brigitte Pientka, Alberto Momigliano. There is also a lot of work about
other simply typed frameworks; e.g. Abella. There is a lot to say about
consistency, expressiveness and usability of frameworks.
You haven't even scratched the surface of logical frameworks.
--Randy
On Mon, Mar 12, 2018 at 7:48 PM, Ken Kubota <m...@kenkubota.de> wrote:
> Dear Members of the Research Community,
>
> Finalizing my overview at http://www.owlofminerva.net/files/fom.pdf
> I would like to ask for major logics and logical frameworks not considered
> yet.
>
> The logical frameworks included now (as logical frameworks, not only object
> logics like Isabelle/HOL) are Isabelle and Metamath. These are also the
> only
> two logical frameworks mentioned by Freek Wiedijk as of 2003, see p. 9 at
> http://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf
>
> Kinds regards,
>
> Ken Kubota
>
> ____________________
>
> Ken Kubota
> http://doi.org/10.4444/100
>
>
>
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
