Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Logical Frameworks
A logical framework is a formal meta-language for deductive systems.
The primary tasks supported in logical frameworks to varying degrees are
specification of deductive systems,
search for derivations within deductive systems,
meta-programming of algorithms pertaining to deductive systems,
proving meta-theorems about deductive systems.
I include here systems that in other places have been called meta-logics and
meta-logical frameworks; for me the choice of terminology merely indicates the
relative emphasis placed on these tasks. Logical frameworks have been applied
to many examples from logic and the theory of programming languages. A short survey on logical
frameworks provides a guide to some papers in this bibliography as
of late 1995. Here are short-cuts to home pages for logical frameworks where
available:
ELAN,
Elf, Forum, Isabelle, lambda Prolog.
Important Disclaimer: In order to keep the task of compiling this
material manageable I excluded general-purpose theorem proving systems
designed for the formalization of classical or constructive mathematics, such
as Coq, HOL, LEGO, Mizar, NQTHM, Nuprl, and
many others.
However, I included individual experiments carried out in these systems that
are meta-logical in nature. I am also providing pointers to home pages for
related systems and topics where
available.