Colouring flags with Dafny & Idris

Research output: Contribution to conferencePaperpeer-review

26 Downloads (Pure)

Abstract

Dafny and Idris are two verification-aware programming languages that support two different styles of fine-grained reasoning about our software programs. Dafny is an imperative design-by-contract language that provides a clear separation between specifications and code, while Idris is a dependently-typed functional language in which specifications are code. Each of these approaches support different styles of verification (Hoare Logic in Dafny versus Dependent Type Theory in Idris). In this paper, we will examine how Dafny and Idris express The Problem of the Dutch National Flag from Dijkstra’s Discipline of Programming and note the differences and similarities between both approaches.
Original languageEnglish
Publication statusPublished - 14 Jan 2024
EventDafny 2024 - Institution of Engineering and Technology, London, United Kingdom
Duration: 14 Jan 202414 Jan 2024
https://popl24.sigplan.org/home/dafny-2024

Conference

ConferenceDafny 2024
Country/TerritoryUnited Kingdom
CityLondon
Period14/01/2414/01/24
Internet address

Keywords

  • Idris
  • Dafny
  • verification
  • dependent types

Fingerprint

Dive into the research topics of 'Colouring flags with Dafny & Idris'. Together they form a unique fingerprint.

Cite this