Verification languages such as, among others, Coq, Lean, Agda, Athena, Liquid Haskell, Maude ,… have become central tools for building reliable software and for advancing formal methods research. While each language has its own community and conference, there is a growing need for a shared forum where researchers can exchange insights across language boundaries.
The First Workshop on Verification Languages aims to bring together researchers, practitioners, and tool developers to discuss common design principles, compare approaches, underlying mathematical theories, capacities, capabilities, and in general share experiences in the development and application of verification languages into modern reliable software systems.
This workshop will be a forum to discuss advances in verification languages and their application, with the objective of breaking the boundaries of a single verification language, that can foster collaboration between researchers of different language backgrounds.
The workshop will feature:
- An invited keynote talk. (TBC)
- Presentations of peer-reviewed papers.
- A Verification Challenge, where participants tackle a proposed challenge using their weapon of choice (e.g., Maude, Adga, Liquid Haskell, Athena…). Then during the workshop we will have space to share/show solutions between the different language, to show case the similarities and differences between verification languages, as possible collaboration points.
This program is tentative and subject to change.
Mon 29 JunDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
Unscheduled Events
| Not scheduled Talk | Proof Primitives for Equality Saturation-based Automated Provers VeriLang George Zakhour , Jahrim Gabriele Cesario University of St. Gallen, Pascal Weisenburger University of St. Gallen, Guido Salvaneschi University of St. Gallen | ||
| Not scheduled Talk | A Case Study in Proving the Soundness and Completeness of Natural Deduction for Propositional Logic in Dafny VeriLang Daniel Bîrleanu Alexandru Ioan Cuza University, Iasi, Ștefan Ciobâcă Alexandru Ioan Cuza University of Iasi |
Accepted Papers
| Title | |
|---|---|
| A Case Study in Proving the Soundness and Completeness of Natural Deduction for Propositional Logic in Dafny VeriLang | |
| Proof Primitives for Equality Saturation-based Automated Provers VeriLang |
Call for Papers
VeriLang seeks submissions of papers discussing the implementation and application of verification languages and their associated tools.
Topics of Interest
We welcome submissions on all aspects of verification languages, including but not limited to:
- Language design and semantics.
- Type systems and logical foundations.
- Integration with automated provers and SMT solvers.
- Tooling, IDEs, Debuggers and usability.
- Verification of software, hardware, and systems.
- Educational use of verification languages.
- Comparative studies of verification languages.
- Case studies and applications.
We invite two categories of submissions:
- Full papers (up to 12 pages, excluding references): Original research contributions, experience reports, or detailed case studies.
- Short papers (up to 6 pages, excluding references): Work-in-progress, new ideas, position papers, or reports on ongoing projects.
Papers accepted for presentation to VeriLang will have a publication at the ACM Digital Library as part of the collaboration between ECOOP and ACM. Therefore, papers should be formatted using the latest version of the ACM proceedings (https://www.sigplan.org/Resources/Author/) using the sigplan subformat.
Paper submission will be though EasyChair: https://easychair.org/conferences/?conf=verilang26
Important note to authors about the new ACM open access publishing model
All papers in the ECOOP-C’26 proceedings will be published open access (OA) on the ACM Digital Library. For authors who are not affiliated with member institutions of the ACM Open Program, ACM charges an article processing charge (APC) for OA publication. However, the ECOOP-C’26 conference committee has agreed that the conference will pay all applicable APCs. All papers will therefore be published OA at no cost to authors.
| Fri 8 May 2026 Camera ready submission |
| Mon 29 Jun 2026 Workshop date |
| Fri 24 Apr 2026 Author notification |
| Sat 14 Mar 2026 Paper submission |
