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

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

• Noah Ohrner, St Catharine's College
• Wednesday 04 December 2019, 19:00-19:30
• Wolfson Hall, Churchill College.

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.

This talk is included in these lists:

• Churchill CompSci Talks
• Wolfson Hall, Churchill College
• computer science
• se393's list

Note that ex-directory lists are not shown.