Nominal Logic: A First Order Theory of Names and Binding Export

@article{citeulike:526442, abstract = {This paper formalises within first-order logic some common practices in computer science to do with representing and reasoning about syntactical structures involving named bound variables (as opposed to nameless terms, explicit substitutions, or higher order abstract syntax). It introduces Nominal Logic, a version of first-order many-sorted logic with equality containing primitives for renaming via name-swapping and for freshness of names, from which a notion of binding can be derived. Its...}, author = {Pitts, Andrew M.}, citeulike-article-id = {526442}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.7844}, journal = {Lecture Notes in Computer Science}, keywords = {dependent\_types, nominal\_logic, type\_theory}, pages = {219--242}, posted-at = {2006-03-02 08:46:25}, priority = {4}, title = {Nominal Logic: A First Order Theory of Names and Binding}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.7844}, volume = {2215}, year = {2001} }

TY - JOUR ID - citeulike:526442 L3 - citeulike-article-id:526442 N2 - This paper formalises within first-order logic some common practices in computer science to do with representing and reasoning about syntactical structures involving named bound variables (as opposed to nameless terms, explicit substitutions, or higher order abstract syntax). It introduces Nominal Logic, a version of first-order many-sorted logic with equality containing primitives for renaming via name-swapping and for freshness of names, from which a notion of binding can be derived. Its... JF - Lecture Notes in Computer Science EP - 242 TI - Nominal Logic: A First Order Theory of Names and Binding VL - 2215 SP - 219 KW - dependent_types KW - nominal_logic KW - type_theory AU - Pitts, Andrew PY - 2001/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.7844 ER -