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: | Text |
Language: | unknown |
Published: |
2017
|
Subjects: | |
Online Access: | http://arxiv.org/abs/1702.02282 https://doi.org/10.4204/EPTCS.241.3 |
id |
ftarxivpreprints:oai:arXiv.org:1702.02282 |
---|---|
record_format |
openpolar |
spelling |
ftarxivpreprints:oai:arXiv.org:1702.02282 2023-09-05T13:19:06+02:00 Dependent Types for Multi-Rate Flows in Synchronous Programming Blair, William Xi, Hongwei 2017-02-07 http://arxiv.org/abs/1702.02282 https://doi.org/10.4204/EPTCS.241.3 unknown http://arxiv.org/abs/1702.02282 EPTCS 241, 2017, pp. 36-44 doi:10.4204/EPTCS.241.3 Computer Science - Programming Languages D.3.3 D.4.7 F.3.1 F.3.3 text 2017 ftarxivpreprints https://doi.org/10.4204/EPTCS.241.3 2023-08-16T14:16:57Z 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. Comment: In Proceedings ML/OCaml 2015, arXiv:1702.01872 Text DML ArXiv.org (Cornell University Library) Electronic Proceedings in Theoretical Computer Science 241 36 44 |
institution |
Open Polar |
collection |
ArXiv.org (Cornell University Library) |
op_collection_id |
ftarxivpreprints |
language |
unknown |
topic |
Computer Science - Programming Languages D.3.3 D.4.7 F.3.1 F.3.3 |
spellingShingle |
Computer Science - Programming Languages D.3.3 D.4.7 F.3.1 F.3.3 Blair, William Xi, Hongwei Dependent Types for Multi-Rate Flows in Synchronous Programming |
topic_facet |
Computer Science - Programming Languages D.3.3 D.4.7 F.3.1 F.3.3 |
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. Comment: In Proceedings ML/OCaml 2015, arXiv:1702.01872 |
format |
Text |
author |
Blair, William Xi, Hongwei |
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 |
publishDate |
2017 |
url |
http://arxiv.org/abs/1702.02282 https://doi.org/10.4204/EPTCS.241.3 |
genre |
DML |
genre_facet |
DML |
op_relation |
http://arxiv.org/abs/1702.02282 EPTCS 241, 2017, pp. 36-44 doi:10.4204/EPTCS.241.3 |
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_ |
1776199922242027520 |