Type-level property based testing

Thomas Ekström Hansen; Edwin Charles Brady

doi:10.1145/3678000.3678206

Type-level property based testing

Thomas Ekström Hansen^*, Edwin Charles Brady

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking and type checking are currently separate techniques for automatically verifying the correctness of programs. Using Property Based Testing (PBT), Indexed State Monads (ISMs), and dependent types, we are able to model several interesting systems and network protocols, have the type checker verify that our implementation behaves as specified, and test that our model matches the specification's semantics; a step towards combining model and type checking.

Original language	English
Title of host publication	TyDe 2024: Proceedings of the 9th ACM SIGPLAN international workshop on type-driven development
Editors	Sandra Alves, Jesper Cockx
Place of Publication	New York
Publisher	ACM
Pages	37 - 49
ISBN (Print)	9798400711039
DOIs	https://doi.org/10.1145/3678000.3678206
Publication status	Published - 28 Aug 2024
Event	Workshop on Type-Driven Development (TyDe 2024) - Milan, Italy Duration: 2 Sept 2024 → 7 Sept 2024 https://icfp24.sigplan.org/home/tyde-2024

Workshop

Workshop	Workshop on Type-Driven Development (TyDe 2024)
Abbreviated title	TyDe 2024
Country/Territory	Italy
City	Milan
Period	2/09/24 → 7/09/24
Internet address	https://icfp24.sigplan.org/home/tyde-2024

Access to Document

10.1145/3678000.3678206

Hansen-2024-Type-level-property-based=TyDE2024-AAM
Copyright © 2024 the owner/author(s). Publication rights licensed to ACM. This work has been made available online in accordance with publisher policies or with permission. Permission for further reuse of this content should be sought from the publisher or the rights holder. This is the author created accepted manuscript following peer review and may differ slightly from the final published version. The final published version of this work is available at: https://doi.org/10.1145/3678000.3678206.
Accepted author manuscript, 611 KB

Type-level property based testing (dataset & code)
Hansen, T. E. (Creator) & Brady, E. C. (Creator), GitHub, 2024
https://github.com/CodingCellist/tyde-24-code
Dataset

Cite this

@inproceedings{40b9970c66fe4dde8e3b6d98524ca569,

title = "Type-level property based testing",

abstract = "We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking and type checking are currently separate techniques for automatically verifying the correctness of programs. Using Property Based Testing (PBT), Indexed State Monads (ISMs), and dependent types, we are able to model several interesting systems and network protocols, have the type checker verify that our implementation behaves as specified, and test that our model matches the specification's semantics; a step towards combining model and type checking.",

author = "Hansen, {Thomas Ekstr{\"o}m} and Brady, {Edwin Charles}",

note = "Funding: UK EPSRC grant EP/T007265/1.; Workshop on Type-Driven Development (TyDe 2024), TyDe 2024 ; Conference date: 02-09-2024 Through 07-09-2024",

year = "2024",

month = aug,

day = "28",

doi = "10.1145/3678000.3678206",

language = "English",

isbn = "9798400711039",

pages = "37 -- 49",

editor = "Sandra Alves and Jesper Cockx",

booktitle = "TyDe 2024: Proceedings of the 9th ACM SIGPLAN international workshop on type-driven development",

publisher = "ACM",

address = "United States",

url = "https://icfp24.sigplan.org/home/tyde-2024",

}

TY - GEN

T1 - Type-level property based testing

AU - Hansen, Thomas Ekström

AU - Brady, Edwin Charles

N1 - Funding: UK EPSRC grant EP/T007265/1.

PY - 2024/8/28

Y1 - 2024/8/28

N2 - We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking and type checking are currently separate techniques for automatically verifying the correctness of programs. Using Property Based Testing (PBT), Indexed State Monads (ISMs), and dependent types, we are able to model several interesting systems and network protocols, have the type checker verify that our implementation behaves as specified, and test that our model matches the specification's semantics; a step towards combining model and type checking.

AB - We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking and type checking are currently separate techniques for automatically verifying the correctness of programs. Using Property Based Testing (PBT), Indexed State Monads (ISMs), and dependent types, we are able to model several interesting systems and network protocols, have the type checker verify that our implementation behaves as specified, and test that our model matches the specification's semantics; a step towards combining model and type checking.

U2 - 10.1145/3678000.3678206

DO - 10.1145/3678000.3678206

M3 - Conference contribution

SN - 9798400711039

SP - 37

EP - 49

BT - TyDe 2024: Proceedings of the 9th ACM SIGPLAN international workshop on type-driven development

A2 - Alves, Sandra

A2 - Cockx, Jesper

PB - ACM

CY - New York

T2 - Workshop on Type-Driven Development (TyDe 2024)

Y2 - 2 September 2024 through 7 September 2024

ER -

Type-level property based testing

Abstract

Workshop

Access to Document

Fingerprint

Datasets

Type-level property based testing (dataset & code)

Cite this