Making it easier to write correct programs
Dependently-typed programming languages, such as Idris and Agda, permit the use of logical properties to constrain the values an expression could take. This allows us to incorporate the proof that a program satisfies certain specifications directly in the program itself, making correctness guarantees an intrinsic part of an implementation. Despite this advantage, developing dependently-typed programs can represent a significant challenge. We present a tool that aids a programmer to enrich a program with correctness guarantees.
Keywords
Refactoring, Dependent-types, Program Transformation, Programming Languages
Staff
[Mun See Chang]{msc2}, [Chris Brown]{cmb21}, [Adam Barwell]{abd23}