Andy Melnikov (nponeccop) wrote,
Andy Melnikov

Dynamic typing - литература

Dynamic typing: syntax and proof theory by Fritz Henglein

We present the dynamically typed λ-calculus, an extension of the statically typed λ-calculus with a special type Dyn and explicit dynamic type coercions corresponding to run-time type tagging and type check-and-untag operations. Programs in run-time typed languages can be interpreted in the dynamically typed λ-calculus via a nondeterministic completion process that inserts explicit coercions and type declarations such that a well-typed term results.

  • Post a new comment


    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.