Abstract

Proving program correctness is becoming an increasingly popular area of research as computers are used in applications where security or correctness is of utmost human or economic importance. However, many current standards require either runtime overhead or providing reference implementations of algorithms in specific languages to feed into logic engines. This talk will explore the applications of refinement types to design a strong type system which can enforce program safety according to a logical specification. The type system will be developed in parallel with a a functional language similar to ML which can model concurrency, mutable state and other imperative programming features, improving on runtime or reference implementation schemes. Lastly, it will mention two languages implementing a similar verification type system and their potential uses in verifying security-critical software we interact with on a daily basis.