Logical Framework

A logical framework is a formal logic intended to serve as the metatheory for inductive definitions of other ("object level") logics or programming languages. Working in a logical framework typically provides some benefit over writing down systems of inference rules on paper; for example, a logical framework may include a primitive notion of variable binding and capture-avoiding substitution, avoiding the need to redefine these concepts in each object-level theory.

Depending on the context, Logical Framework can also refer to one of a number of specific logical frameworks, most often ELF or MLLF. de Bruijn's Automath system is widely regarded as the first logical framework.

Edinburgh Logical Framework (ELF or LF)

Please expand.

Harper, Robert and Honsell, Furio and Plotkin, Gordon. A Framework For Defining Logics. Journal of the Association for Computing Machinery, 40(1):143-184, 1993.

@article{10.1145/138027.138060,
author = {Harper, Robert and Honsell, Furio and Plotkin, Gordon},
title = {A Framework for Defining Logics},
year = {1993},
issue_date = {Jan. 1993},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {40},
number = {1},
issn = {0004-5411},
url = {https://doi.org/10.1145/138027.138060},
doi = {10.1145/138027.138060},
journal = {J. ACM},
month = jan,
pages = {143–184},
numpages = {42},
}

Martin-Löf Logical Framework (MLLF)

Please expand.