Data

Tools

Indexes

Applications

Experiments

Open Source Science

dafny-well-behaved-coalgebraic-semantics

Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny

https://github.com/zetzschest/dafny-well-behaved-coalgebraic-semantics

Science Score: 67.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • ✓
    CITATION.cff file
    Found CITATION.cff file
  • ✓
    codemeta.json file
    Found codemeta.json file
  • ✓
    .zenodo.json file
    Found .zenodo.json file
  • ✓
    DOI references
    Found 1 DOI reference(s) in README
  • ✓
    Academic publication links
    Links to: springer.com
  • ○
    Academic email domains
  • ○
    Institutional organization owner
  • ○
    JOSS paper metadata
  • ○
    Scientific vocabulary similarity
    Low similarity (6.1%) to scientific vocabulary
Last synced: 6 months ago · JSON representation ·

Repository

Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny

Basic Info
  • Host: GitHub
  • Owner: zetzschest
  • Language: Dafny
  • Default Branch: main
  • Homepage:
  • Size: 9.77 KB
Statistics
  • Stars: 0
  • Watchers: 1
  • Forks: 0
  • Open Issues: 0
  • Releases: 0
Created over 1 year ago · Last pushed over 1 year ago
Metadata Files
Readme Citation

README.md

Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny

Regular expressions are commonly understood in terms of their denotational semantics, that is, through formal languages -- the regular languages. This view is inductive in nature: two primitives are equivalent if they are constructed in the same way. Alternatively, regular expressions can be understood in terms of their operational semantics, that is, through deterministic finite automata. This view is coinductive in nature: two primitives are equivalent if they are deconstructed in the same way. It is implied by Kleene's famous theorem that both views are equivalent: regular languages are precisely the formal languages accepted by deterministic finite automata. In this paper, we use Dafny, a verification-aware programming language, to formally verify, for the first time, what has been previously established only through proofs-by-hand: the two semantics of regular expressions are well-behaved, in the sense that they are in fact one and the same, up to pointwise bisimilarity. At each step of our formalisation, we propose an interpretation in the language of Coalgebra. We found that Dafny is particularly well suited for the task due to its inductive and coinductive features and hope our approach serves as a blueprint for future generalisations to other theories.

This repository contains the source code accompanying the paper Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny by Stefan Zetzsche and Wojciech Różowski. To cite this repository you can currently use the following reference: @software{Zetzsche_Well-Behaved_Co_algebraic_Semantics_2024, author = {Zetzsche, Stefan and Rozowski, Wojciech}, title = {{Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny}}, url = {https://github.com/zetzschest/dafny-well-behaved-coalgebraic-semantics}, year = {2024} }

Owner

  • Login: zetzschest
  • Kind: user

Citation (CITATION.cff) 

cff-version: 1.2.0
message: "If you use this software, please cite it as below."
authors:
- family-names: "Zetzsche"
  given-names: "Stefan"
- family-names: "Rozowski"
  given-names: "Wojciech"
title: "Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny"
url: "https://github.com/zetzschest/dafny-well-behaved-coalgebraic-semantics"
preferred-citation:
  type: software
  authors:
  - family-names: "Zetzsche"
    given-names: "Stefan"
  - family-names: "Rozowski"
    given-names: "Wojciech"
  title: "Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny"
  url: "https://github.com/zetzschest/dafny-well-behaved-coalgebraic-semantics"
  year: 2024

GitHub Events

Total
  • Push event: 2
Last Year
  • Push event: 2