Self-Quotation in a Typed, Intensional Lambda-Calculus | Zendy

Barry Jay | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Self-Quotation in a Typed, Intensional Lambda-Calculus

Author(s) -

Barry Jay

Publication year - 2018

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2018.03.024

Subject(s) - combinatory logic , typed lambda calculus , lambda calculus , simply typed lambda calculus , church encoding , computer science , system f , programming language , mathematical proof , calculus (dental) , dependent type , algebra over a field , mathematics , pure mathematics , medicine , dentistry , geometry

Intensional lambda-calculus adds intensional combinators to lambda-calculus to facilitate analysis. In particular, they are used to factorise data structures and programs into their components, which can be used to convert abstractions into combinators. This paper shows how to type an intensional lambda-calculus using no more than the types of System F. Even the quotation function used to access program syntax can be defined and typed, as can its inverse: the calculus supports typed self-quotation. Thus, one may freely alternate between program analysis and program execution. Proofs of all results have been verified in Coq.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research