3
$\begingroup$

I'm looking for a logical framework in which it is possible to easily present both intensional and extensional theories of dependent types with a partially ordered set of universes à la Russell satisfying a cumulativity relation (like $\mathsf{Set}$, $\mathsf{Prop}$ and $\mathsf{Type}_i$ in the Calculus of Inductive Constructions). It should serve as a metalanguage for theories such as variations of both Martin-Löf's type theory $\mathrm{ML}$ and $\mathrm{CIC}$.

I'm not satisfied with Martin-Löf's logical framework (by Nordström, Petersson and Smith), nor with its typed version (by Luo), because they are designed to treat universes à la Tarski, which I find quite cumbersome. I'm also not very keen on the Edinburgh logical framework (by Harper, Honsell and Plotkin), mostly because it sacrifices easiness of use in exchange for a generality I think I won't need.

Since I haven't been able to find any relevant articles on this matter, I'll be thankful to anyone who could point me to any helpful references. Thank you.

Improve this question
$\endgroup$
2
  • $\begingroup$ For clarification, what is a "logical framework?" $\endgroup$
    – Noah Schweber
    Commented Feb 10, 2015 at 21:17
  • $\begingroup$ 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. $\endgroup$
    – Luca Bressan
    Commented Feb 10, 2015 at 21:32

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .