Formalising a Structural, Gradual, Pluggable Type System
ECS PhD Proposal
Speaker: Tim Jones
Time: Friday 12th July 2013 at 01:00 PM - 02:00 PM
Location: Cotton Club, Cotton 350
Formal modelling of programming language concepts offer strong mathematical reasoning and definitive proofs of properties, but most languages are not thoroughly formalised. Models applied to existing implementations often discover unsound edge cases in the language design, but producing a formalism to be used as a language specification is a difficult task and the cost of maintaining it can hinder further experimentation.
This talk will cover our proposal to formally model Grace, a programming language with a design based in popular, modern paradigms and a type system with features that have been formalised individually but not combined. We intend to investigate how the language's extensibility features can offer us a chance to simplify and automate the formalisation procedure, making it easer to produce programming languages that are more correct and complete.