Formalizing Domains, Ultrametric Spaces and Semantics of Programming Languages
Source: Carnegie Mellon University
The use of proof assistants in formalizing language meta-theory and implementing certified tools has grown enormously over the last decade, and is now a major trend in programming language research. Most current work on mechanizing language definitions and safety proofs, certified compilation, proof carrying code, and so on uses fairly elementary operational methods, such as syntactic type soundness and rather intensional simulation relations for compiler correctness. Indeed, one of the motivations for the recent development of some of the most exciting new operational methods, notably step-indexing and its refinements, has been a desire for techniques that are more amenable to machine formalization than is domain theory, which has often been viewed as too complex to work with in a proof assistant.