nopeA Framework for Defining Logics
(1993) : Harper, Robert Honsell, Furio ...
DOI: https://doi.org/10.1145/138027.138060
#LF #proof_search #theorem_proving #formal_methods #judgement #lambda_calculus #edinburgh_logical_framework #my_bibtex
(1993) : Harper, Robert Honsell, Furio ...
DOI: https://doi.org/10.1145/138027.138060
#LF #proof_search #theorem_proving #formal_methods #judgement #lambda_calculus #edinburgh_logical_framework #my_bibtex
A framework for defining logics | Journal of the ACM
The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent types. Syntax is treated in a style similar to, but more ...