Lambda Calculus Models of Programming Languages
Two aspects of programming languages, recursive definitions and type declarations are analyzed in detail. Church's -calculus is used as a model of a programming language for purposes of the analysis. The main result on recursion is an analogue to Kleene's first recursion theorem: If A= F...
| Main Author: | |
|---|---|
| Other Authors: | |
| Published: |
2023
|
| Online Access: | https://hdl.handle.net/1721.1/149376 |
| _version_ | 1811068886993338368 |
|---|---|
| author | Morris, James H. |
| author2 | Wozencraft, John M. |
| author_facet | Wozencraft, John M. Morris, James H. |
| author_sort | Morris, James H. |
| collection | MIT |
| description | Two aspects of programming languages, recursive definitions and type declarations are analyzed in detail. Church's -calculus is used as a model of a programming language for purposes of the analysis. The main result on recursion is an analogue to Kleene's first recursion theorem: If A= FA for any A-expressions A and F, then A is an extension of YF in the sense that if E[YE], any expressions containing YF, has a normal form then E[F] =E {A]. Y is Curry's paradoxical combinator. The result is shown to be invariant for many different versions of Y. |
| first_indexed | 2024-09-23T08:02:31Z |
| id | mit-1721.1/149376 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T08:02:31Z |
| publishDate | 2023 |
| record_format | dspace |
| spelling | mit-1721.1/1493762023-03-30T04:25:10Z Lambda Calculus Models of Programming Languages Morris, James H. Wozencraft, John M. Two aspects of programming languages, recursive definitions and type declarations are analyzed in detail. Church's -calculus is used as a model of a programming language for purposes of the analysis. The main result on recursion is an analogue to Kleene's first recursion theorem: If A= FA for any A-expressions A and F, then A is an extension of YF in the sense that if E[YE], any expressions containing YF, has a normal form then E[F] =E {A]. Y is Curry's paradoxical combinator. The result is shown to be invariant for many different versions of Y. 2023-03-29T14:53:52Z 2023-03-29T14:53:52Z 1968-12 https://hdl.handle.net/1721.1/149376 00114444 MIT-LCS-TR-057 MAC-TR-057 application/pdf |
| spellingShingle | Morris, James H. Lambda Calculus Models of Programming Languages |
| title | Lambda Calculus Models of Programming Languages |
| title_full | Lambda Calculus Models of Programming Languages |
| title_fullStr | Lambda Calculus Models of Programming Languages |
| title_full_unstemmed | Lambda Calculus Models of Programming Languages |
| title_short | Lambda Calculus Models of Programming Languages |
| title_sort | lambda calculus models of programming languages |
| url | https://hdl.handle.net/1721.1/149376 |
| work_keys_str_mv | AT morrisjamesh lambdacalculusmodelsofprogramminglanguages |