Dependent types for multi-rate flows in synchronous programming
Synchronous programming languages emerged in the 1980s as tools for implementing reactive systems, which interact with events from physical environments and often must do so under strict timing constraints. In this report, we encode inside ATS various real-time primitives in an experimental synchron...
Published in: | Electronic Proceedings in Theoretical Computer Science |
---|---|
Main Authors: | , |
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
Open Publishing Association
2017
|
Subjects: | |
Online Access: | https://hdl.handle.net/2144/44998 https://doi.org/10.4204/eptcs.241.3 |
id |
ftbostonuniv:oai:open.bu.edu:2144/44998 |
---|---|
record_format |
openpolar |
spelling |
ftbostonuniv:oai:open.bu.edu:2144/44998 2023-05-15T16:01:54+02:00 Dependent types for multi-rate flows in synchronous programming Blair, William Xi, Hongwei 2017-02-07 p. 36 - 44 https://hdl.handle.net/2144/44998 https://doi.org/10.4204/eptcs.241.3 en en_US eng Open Publishing Association Electronic Proceedings in Theoretical Computer Science W. Blair, H. Xi. "Dependent Types for Multi-Rate Flows in Synchronous Programming." Electronic Proceedings in Theoretical Computer Science, Volume 241, pp. 36 - 44. https://doi.org/10.4204/eptcs.241.3 2075-2180 https://hdl.handle.net/2144/44998 doi:10.4204/eptcs.241.3 185116 © William Blair & Hongwei Xi. This work is licensed under the Creative Commons Attribution License. http://creativecommons.org/licenses/by/4.0/ CC-BY Article 2017 ftbostonuniv https://doi.org/10.4204/eptcs.241.3 2022-08-20T22:18:13Z Synchronous programming languages emerged in the 1980s as tools for implementing reactive systems, which interact with events from physical environments and often must do so under strict timing constraints. In this report, we encode inside ATS various real-time primitives in an experimental synchronous language called Prelude, where ATS is a statically typed language with an ML-like functional core that supports both dependent types (of DML-style) and linear types. We show that the verification requirements imposed on these primitives can be formally expressed in terms of dependent types in ATS. Moreover, we modify the Prelude compiler to automatically generate ATS code from Prelude source. This modified compiler allows us to solely rely on typechecking in ATS to discharge proof obligations originating from the need to typecheck Prelude code. Whereas ATS is typically used as a general purpose programming language, we hereby demonstrate that it can also be conveniently used to support some forms of advanced static checking in languages equipped with less expressive types. Published version Article in Journal/Newspaper DML Boston University: OpenBU Electronic Proceedings in Theoretical Computer Science 241 36 44 |
institution |
Open Polar |
collection |
Boston University: OpenBU |
op_collection_id |
ftbostonuniv |
language |
English |
description |
Synchronous programming languages emerged in the 1980s as tools for implementing reactive systems, which interact with events from physical environments and often must do so under strict timing constraints. In this report, we encode inside ATS various real-time primitives in an experimental synchronous language called Prelude, where ATS is a statically typed language with an ML-like functional core that supports both dependent types (of DML-style) and linear types. We show that the verification requirements imposed on these primitives can be formally expressed in terms of dependent types in ATS. Moreover, we modify the Prelude compiler to automatically generate ATS code from Prelude source. This modified compiler allows us to solely rely on typechecking in ATS to discharge proof obligations originating from the need to typecheck Prelude code. Whereas ATS is typically used as a general purpose programming language, we hereby demonstrate that it can also be conveniently used to support some forms of advanced static checking in languages equipped with less expressive types. Published version |
format |
Article in Journal/Newspaper |
author |
Blair, William Xi, Hongwei |
spellingShingle |
Blair, William Xi, Hongwei Dependent types for multi-rate flows in synchronous programming |
author_facet |
Blair, William Xi, Hongwei |
author_sort |
Blair, William |
title |
Dependent types for multi-rate flows in synchronous programming |
title_short |
Dependent types for multi-rate flows in synchronous programming |
title_full |
Dependent types for multi-rate flows in synchronous programming |
title_fullStr |
Dependent types for multi-rate flows in synchronous programming |
title_full_unstemmed |
Dependent types for multi-rate flows in synchronous programming |
title_sort |
dependent types for multi-rate flows in synchronous programming |
publisher |
Open Publishing Association |
publishDate |
2017 |
url |
https://hdl.handle.net/2144/44998 https://doi.org/10.4204/eptcs.241.3 |
genre |
DML |
genre_facet |
DML |
op_relation |
Electronic Proceedings in Theoretical Computer Science W. Blair, H. Xi. "Dependent Types for Multi-Rate Flows in Synchronous Programming." Electronic Proceedings in Theoretical Computer Science, Volume 241, pp. 36 - 44. https://doi.org/10.4204/eptcs.241.3 2075-2180 https://hdl.handle.net/2144/44998 doi:10.4204/eptcs.241.3 185116 |
op_rights |
© William Blair & Hongwei Xi. This work is licensed under the Creative Commons Attribution License. http://creativecommons.org/licenses/by/4.0/ |
op_rightsnorm |
CC-BY |
op_doi |
https://doi.org/10.4204/eptcs.241.3 |
container_title |
Electronic Proceedings in Theoretical Computer Science |
container_volume |
241 |
container_start_page |
36 |
op_container_end_page |
44 |
_version_ |
1766397584704798720 |