@article{popescu-rosu-2015-jtcs,
author = {Andrei Popescu and Grigore Ro\c{s}u},
title = {Term-Generic Logic},
abstract = {
We introduce term-generic logic (TGL), a first-order logic
parameterized with terms defined axiomatically (rather than
constructively), by requiring terms to only provide
free variable and substitution operators satisfying some reasonable axioms.
TGL has a notion of model that generalizes both first-order models
and Henkin models of the lambda-calculus. The abstract notions of term syntax and model
are shown to be sufficient for obtaining
the completeness theorem of a Gentzen system generalizing that of first-order logic.
Various systems featuring bindings and contextual reasoning,
ranging from pure type systems to the pi-calculus,
are captured as theories inside TGL.
For two particular, but rather typical instances---untyped lambda-calculus and
System F---the general-purpose TGL models are shown to be equivalent with
standard ad hoc models.
},
journal = {Theoretical Computer Science},
volume = 577,
number = 1,
month = {April},
pages = {1-24},
year = {2015},
doi = {http://dx.doi.org/10.1016/j.tcs.2015.01.047},
author_id = {Andrei Popescu and Grigore Rosu},
category = {fsl, semantics, logics, programming_languages},
journal_acronym = {Journal of Theoretical Computer Science},
journal_url = {http://www.journals.elsevier.com/theoretical-computer-science/},
project_acronym = {GFOL},
project_url = {http://fsl.cs.illinois.edu/index.php/Generic_First-Order_Logic},
}