Barwell, Adam D., Brown, Christopher, Chang, Mun See, Theocharis, Constantine, Thompson, Simon (2025) Structural Refactorings for Exploring Dependently Typed Programming. In: Lecture Notes in Computer Science. Trends in Functional Programming. 25th International Symposium, TFP 2024, South Orange, NJ, USA, January 10–12, 2024, Revised Selected Papers. 14843. pp. 1-21. Springer ISBN 978-3-031-74557-7. (doi:10.1007/978-3-031-74558-4_1) (KAR id:108420)
|
PDF
Author's Accepted Manuscript
Language: English 
This work is licensed under a Creative Commons Attribution 4.0 International License.
|
|
|
Download this file (PDF/650kB) |
Preview |
| Request a format suitable for use with assistive technology e.g. a screenreader | |
| Official URL: https://doi.org/10.1007/978-3-031-74558-4_1 |
|
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.
| Item Type: | Conference or workshop item (Proceeding) |
|---|---|
| DOI/Identification number: | 10.1007/978-3-031-74558-4_1 |
| Uncontrolled keywords: | Refactoring, Dependent Types, Program Transformation |
| Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science |
| Institutional Unit: | Schools > School of Computing |
| Former Institutional Unit: |
Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
|
| Funders: | University of Kent (https://ror.org/00xkeyj56) |
| Depositing User: | Simon Thompson |
| Date Deposited: | 14 Jan 2025 18:03 UTC |
| Last Modified: | 22 Jul 2025 09:22 UTC |
| Resource URI: | https://kar.kent.ac.uk/id/eprint/108420 (The current URI for this page, for reference purposes) |
University of Kent Author Information
Thompson, Simon.
| Creator's ORCID: |
 https://orcid.org/0000-0002-2350-301X
|
|---|---|
| CReDIT Contributor Roles: |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):
Altmetric
Altmetric
