a lambda-free logical framework Export

@misc{citeulike:1432342, abstract = {A lambda-free logical framework takes parameterisation and definitions as the basic notions to provide schematic mechanisms for specification of type theories and their use in practice. The framework presented here, PAL + , is a logical framework for specification and implementation of type theories, such as Martin-Lof's type theory or UTT. As in Martin-Lof's logical framework [NPS90], computational rules can be introduced and are used to give meanings to the declared constants. However, ...}, author = {Luo, Z.}, citeulike-article-id = {1432342}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.8715}, keywords = {cs, lf}, posted-at = {2007-07-04 06:33:16}, priority = {4}, title = {a lambda-free logical framework}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.8715}, year = {2000} }

TY - GEN ID - citeulike:1432342 L3 - citeulike-article-id:1432342 N2 - A lambda-free logical framework takes parameterisation and definitions as the basic notions to provide schematic mechanisms for specification of type theories and their use in practice. The framework presented here, PAL + , is a logical framework for specification and implementation of type theories, such as Martin-Lof's type theory or UTT. As in Martin-Lof's logical framework [NPS90], computational rules can be introduced and are used to give meanings to the declared constants. However, ... TI - a lambda-free logical framework KW - cs KW - lf AU - Luo, Z PY - 2000/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.8715 ER -