Picture water droplets

Developing mathematical theories of the physical world: Open Access research on fluid dynamics from Strathclyde

Strathprints makes available Open Access scholarly outputs by Strathclyde's Department of Mathematics & Statistics, where continuum mechanics and industrial mathematics is a specialism. Such research seeks to understand fluid dynamics, among many other related areas such as liquid crystals and droplet evaporation.

The Department of Mathematics & Statistics also demonstrates expertise in population modelling & epidemiology, stochastic analysis, applied analysis and scientific computing. Access world leading mathematical and statistical Open Access research!

Explore all Strathclyde Open Access research...

Type-and-scope safe programs and their proofs

Allais, Guillaume and Chapman, James and McBride, Conor and McKinna, James (2017) Type-and-scope safe programs and their proofs. In: CPP 2017. ACM, New York, NY, New York. ISBN 9781450347051

[img]
Preview
Text (Allais-etal-CPP-2017-Type-and-scope-safe-programs)
Allais_etal_CPP_2017_Type_and_scope_safe_programs.pdf
Accepted Author Manuscript

Download (158kB) | Preview

Abstract

We abstract the common type-and-scope safe structure fromcomputations on lambda-terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing witha name supply. By exposing this structure, we can prove generic simulation and fusion lemmas relating operations built this way. This work has been fully formalised in Agda.