University of Cambridge > Talks.cam > Churchill CompSci Talks > On the Use of Typing for Static Logical Verification: RCF and Refinement Types

On the Use of Typing for Static Logical Verification: RCF and Refinement Types

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Matthew Ireland.

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.

This talk is part of the Churchill CompSci Talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity