posted on 2009-06-01, 00:00authored byIliano Cervesato
I was recently invited to give a presentation about the logical framework LLF}. After a 40 minutes talk in which I revealed the intricacies of the underlying type theory and illustrated by means of examples the meta-representation wonders of this new language, somebody in the audience said: "This looks very complicated. Why not using, say, classical logic instead?". In this chapter, I build upon my then improvised answer. I will recall what logical frameworks are and try to motivate the simple but unfamiliar constructs they often rely upon.