Verified Metatheory and Type Inference for a Simply-Typed, Name-Carrying Lambda Calculus

by Rawson, Michael Ian, BA

Abstract (Summary)
I aim to create a mechanisation in Isabelle of the simply-typed λ-calculus, together with a verified algorithm for type inference. Emphasis is placed on the treatment of binders in the calculus and the approach taken with representing α-equivalence.
Full Text Links

Main Document: View

Bibliographical Information:

Advisor:Dominic Mulligan, Victor Gomes

School:University of Cambridge

School Location:United Kingdom

Source Type:Other

Keywords:lambda-calculus, Isabelle, type-inference


Date of Publication:05/19/2017

© 2009 All Rights Reserved.