We are inviting IDEALS users, both people looking for materials in IDEALS and those who want to deposit their work, to give us feedback on improving this service through an interview. Participants will receive a $20 VISA gift card. Please sign up via webform.
Files in this item
|(no description provided)|
|Author(s):||Popescu, Andrei; Rosu, Grigore|
|Abstract:||Term-generic logic (TGL) is a first-order logic parameterized with terms defined axiomatically (rather than constructively), by requiring them to only provide generic notions of free variable and substitution satisfying reasonable properties. TGL has a complete Gentzen system generalizing that of first-order logic. A certain fragment of TGL, called Horn^2 possesses a much simpler Gentzen system, similar to traditional typing derivation systems of lambda-calculi. Horn^2 appears to be sufficient for defining a whole plethora of lambda-calculi as theories inside the logic. Within intuitionistic TGL, a Horn^2 specification of a calculus is likely to be adequate by default. A bit of extra effort shows adequacy w.r.t. classic TGL as well, endowing the calculus with a complete loose semantics.|
|Date Available in IDEALS:||2009-04-14|