Timeline for Logical framework for type theories like ML and CIC
Current License: CC BY-SA 3.0
4 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Feb 10, 2015 at 21:32 | comment | added | Luca Bressan | I guess there is no universally accepted definition of "logical framework". Basically, a logical framework is a metalanguage by means of which one can present a particular type theory through a set of axioms (i.e. typings of constants and equalities). It is usually formalized as a type theory itself, but it doesn't necessarily possess the same features of the theories that one defines in it. | |
Feb 10, 2015 at 21:17 | comment | added | Noah Schweber | For clarification, what is a "logical framework?" | |
Feb 10, 2015 at 19:34 | history | migrated | from math.stackexchange.com (revisions) | ||
Feb 8, 2015 at 16:29 | history | asked | Luca Bressan | CC BY-SA 3.0 |