Structural refactorings for exploring dependently typed programming

Adam David Barwell; Christopher Mark Brown; Mun See Chang; Constantine Theocharis; Simon Thompson

doi:10.1007/978-3-031-74558-4_1

Structural refactorings for exploring dependently typed programming

Adam David Barwell, Christopher Mark Brown^*, Mun See Chang, Constantine Theocharis, Simon Thompson

^*Corresponding author for this work

School of Computer Science

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

Abstract

Dependent types provide users with the tools to embody specifications in types, with implementations carrying proofs that the specifications are met. One approach to developing programs in a dependently typed language develops such programs by enriching simply typed programs through a process of refactoring.

Original language	English
Title of host publication	Trends in functional programming
Subtitle of host publication	25th International Symposium, TFP 2024, South Orange, NJ, USA, January 10–12, 2024, revised selected papers
Editors	Jason Hemann, Stephen Chang
Place of Publication	Cham
Publisher	Springer
Pages	1-21
ISBN (Electronic)	9783031745584
ISBN (Print)	9783031745577
DOIs	https://doi.org/10.1007/978-3-031-74558-4_1
Publication status	Published - 10 Jan 2025
Event	25th International Symposium on Trends in Functional Programming - South Orange, United States Duration: 9 Jan 2024 → 12 Jan 2024 Conference number: 25 https://trendsfp.github.io/2024/

Publication series

Name	Lecture notes in computer science
Publisher	Springer Nature
Volume	14843
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	25th International Symposium on Trends in Functional Programming
Abbreviated title	TFP (and TFPiE) 2024
Country/Territory	United States
City	South Orange
Period	9/01/24 → 12/01/24
Internet address	https://trendsfp.github.io/2024/

Keywords

Refactoring
Dependent types
Program transformation

Access to Document

10.1007/978-3-031-74558-4_1

Barwell-2025-Structural-refactorings-for-exploring-TFP204-AAM-CCBY
Copyright © 2025 the Authors. This accepted manuscript is distributed under the terms of the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original author and source are credited. The final published version of this work is available at https://doi.org/10.1007/978-3-031-74558-4_1.
Accepted author manuscript, 524 KBLicence: CC BY

Energise: Refactorings and Skeletons for: Energise: Refactorings and Skeletons for Energy-Aware Applications on High-Performance Embedded Systems
Brown, C. M. (PI)
EPSRC
1/04/21 → 31/03/24
Project: Standard

Structural refactorings for exploring dependently typed programming (code)
Barwell, A. D. (Creator), Brown, C. M. (Creator), Chang, M. S. (Creator) & Theocharis, K. (Creator), GitHub, 2025
https://github.com/kontheocharis/fluid
Dataset: Software

Cite this

Barwell, A. D., Brown, C. M., Chang, M. S., Theocharis, C., & Thompson, S. (2025). Structural refactorings for exploring dependently typed programming. In J. Hemann, & S. Chang (Eds.), Trends in functional programming: 25th International Symposium, TFP 2024, South Orange, NJ, USA, January 10–12, 2024, revised selected papers (pp. 1-21). (Lecture notes in computer science; Vol. 14843). Springer. https://doi.org/10.1007/978-3-031-74558-4_1

Barwell, Adam David ; Brown, Christopher Mark ; Chang, Mun See et al. / Structural refactorings for exploring dependently typed programming. Trends in functional programming: 25th International Symposium, TFP 2024, South Orange, NJ, USA, January 10–12, 2024, revised selected papers. editor / Jason Hemann ; Stephen Chang. Cham : Springer, 2025. pp. 1-21 (Lecture notes in computer science).

@inproceedings{d0af4287bf894cfba3e4c5593c042b8f,

title = "Structural refactorings for exploring dependently typed programming",

abstract = "Dependent types provide users with the tools to embody specifications in types, with implementations carrying proofs that the specifications are met. One approach to developing programs in a dependently typed language develops such programs by enriching simply typed programs through a process of refactoring.",

keywords = "Refactoring, Dependent types, Program transformation",

author = "Barwell, {Adam David} and Brown, {Christopher Mark} and Chang, {Mun See} and Constantine Theocharis and Simon Thompson",

note = "Funding: This work was supported by UK EPSRC, EP/V006290/1.; 25th International Symposium on Trends in Functional Programming, TFP (and TFPiE) 2024 ; Conference date: 09-01-2024 Through 12-01-2024",

year = "2025",

month = jan,

day = "10",

doi = "10.1007/978-3-031-74558-4_1",

language = "English",

isbn = "9783031745577",

series = "Lecture notes in computer science",

publisher = "Springer",

pages = "1--21",

editor = "Jason Hemann and Stephen Chang",

booktitle = "Trends in functional programming",

address = "Netherlands",

url = "https://trendsfp.github.io/2024/",

}

Barwell, AD , Brown, CM , Chang, MS , Theocharis, C & Thompson, S 2025, Structural refactorings for exploring dependently typed programming. in J Hemann & S Chang (eds), Trends in functional programming: 25th International Symposium, TFP 2024, South Orange, NJ, USA, January 10–12, 2024, revised selected papers. Lecture notes in computer science, vol. 14843, Springer, Cham, pp. 1-21, 25th International Symposium on Trends in Functional Programming, South Orange, New Jersey, United States, 9/01/24. https://doi.org/10.1007/978-3-031-74558-4_1

Structural refactorings for exploring dependently typed programming. / Barwell, Adam David ; Brown, Christopher Mark ; Chang, Mun See et al.
Trends in functional programming: 25th International Symposium, TFP 2024, South Orange, NJ, USA, January 10–12, 2024, revised selected papers. ed. / Jason Hemann; Stephen Chang. Cham: Springer, 2025. p. 1-21 (Lecture notes in computer science; Vol. 14843).

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

TY - GEN

T1 - Structural refactorings for exploring dependently typed programming

AU - Barwell, Adam David

AU - Brown, Christopher Mark

AU - Chang, Mun See

AU - Theocharis, Constantine

AU - Thompson, Simon

N1 - Conference code: 25

PY - 2025/1/10

Y1 - 2025/1/10

N2 - Dependent types provide users with the tools to embody specifications in types, with implementations carrying proofs that the specifications are met. One approach to developing programs in a dependently typed language develops such programs by enriching simply typed programs through a process of refactoring.

AB - Dependent types provide users with the tools to embody specifications in types, with implementations carrying proofs that the specifications are met. One approach to developing programs in a dependently typed language develops such programs by enriching simply typed programs through a process of refactoring.

KW - Refactoring

KW - Dependent types

KW - Program transformation

U2 - 10.1007/978-3-031-74558-4_1

DO - 10.1007/978-3-031-74558-4_1

M3 - Conference contribution

SN - 9783031745577

T3 - Lecture notes in computer science

SP - 1

EP - 21

BT - Trends in functional programming

A2 - Hemann, Jason

A2 - Chang, Stephen

PB - Springer

CY - Cham

T2 - 25th International Symposium on Trends in Functional Programming

Y2 - 9 January 2024 through 12 January 2024

ER -

Barwell AD , Brown CM , Chang MS , Theocharis C, Thompson S. Structural refactorings for exploring dependently typed programming. In Hemann J, Chang S, editors, Trends in functional programming: 25th International Symposium, TFP 2024, South Orange, NJ, USA, January 10–12, 2024, revised selected papers. Cham: Springer. 2025. p. 1-21. (Lecture notes in computer science). doi: 10.1007/978-3-031-74558-4_1

Structural refactorings for exploring dependently typed programming

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Projects

Energise: Refactorings and Skeletons for: Energise: Refactorings and Skeletons for Energy-Aware Applications on High-Performance Embedded Systems

Datasets

Structural refactorings for exploring dependently typed programming (code)

Cite this