A Case Study in Proving the Soundness and Completeness of Natural Deduction for Propositional Logic in Dafny (VeriLang 2026)

Mon 29 June - Fri 3 July 2026 Brussels, Belgium

Who

Daniel Bîrleanu, Ștefan Ciobâcă

Track

VeriLang 2026

This program is tentative and subject to change.

Time Zone

The program is currently displayed in (GMT+02:00) Brussels, Copenhagen, Madrid, Paris.

Use conference time zone: (GMT+02:00) Brussels, Copenhagen, Madrid, ParisSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Mon 29 Jun 2026 11:00 - 11:30 at I.1.07 - Session 2 Chair(s): Mateo Sanabria

Abstract

We present a Dafny formalization of natural deduction for a deep embedding of propositional logic. We present machine-checked proofs of soundness and completeness. We report on our experience of using AI to help speed up the development process.

Daniel Bîrleanu

Alexandru Ioan Cuza University, Iasi

Ștefan Ciobâcă

Alexandru Ioan Cuza University of Iasi

Romania