research-article

An abstract categorical semantics for functional reactive programming with processes

Author:

Wolfgang JeltschAuthors Info & Claims

PLPV '14: Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages meets Program Verification

Pages 47 - 58

https://doi.org/10.1145/2541568.2541573

Published: 11 January 2014 Publication History

Get Access

Abstract

Linear-time temporal logic and functional reactive programming (FRP) are related via a Curry-Howard correspondence. Thereby proofs of "always," "eventually," and "until" propositions correspond to behaviors, events, and processes, respectively. Processes in the FRP sense combine continuous and discrete aspects and generalize behaviors and events. In this paper, we develop a class of axiomatically defined categorical models of FRP with processes. We call these models abstract process categories (APCs). We relate APCs to other categorical models of FRP, namely temporal categories and concrete process categories.

References

[1]

G. Bellin, V. de Paiva, and E. Ritter. Extended Curry-Howard correspondence for a basic constructive modal logic. In Proceedings of the 2nd Workshop on Methods for Modalities (M4M-2), 2001.

Google Scholar

[2]

G. Bierman and V. de Paiva. On an intuitionistic modal logic. Studia Logica, 65 (3): 383--416, Aug. 2000. ISSN 0039-3215. 10.1023/A:1005291931660.

Crossref

Google Scholar

[3]

J. R. B. Cockett and R. A. G. Seely. Linearly distributive functors. Journal of Pure and Applied Algebra, 143 (1--3): 155--203, Nov. 1999. ISSN 0022-4049. 10.1016/S0022-4049(98)00110-8.

Crossref

Google Scholar

[4]

N. Ghani and T. Uustalu. Coproducts of ideal monads. RAIRO Theoretical Informatics and Applications, 38 (4): 321--342, Oct. 2004. ISSN 0988-3754. 10.1051/ita:2004016.

Crossref

Google Scholar

[5]

P. Hudak, A. Courtney, H. Nilsson, and J. Peterson. Arrows, robots, and functional reactive programming. In J. Jeuring and S. Peyton Jones, editors, Advanced Functional Programming, volume 2638 of phLecture Notes in Computer Science, pages 159--187. Springer, Berlin/Heidelberg, Germany, 2003. ISBN 978-3-540-40132-2. 10.1007/978-3-540-44833-4_6.

Crossref

Google Scholar

[6]

A. Jeffrey. LTL types FRP: Linear-time temporal logic propositions as types, proofs as functional reactive programs. In Proceedings of the Sixth Workshop on Programming Languages Meets Program Verification (PLPV '12), pages 49--60, New York, 2012. ACM. ISBN 978-1-4503-1125-0. 10.1145/2103776.2103783.

Digital Library

Google Scholar

[7]

W. Jeltsch. Towards a common categorical semantics for linear-time temporal logic and functional reactive programming. Electronic Notes in Theoretical Computer Science, 286: 229--242, Sept. 2012. ISSN 1571-0661. 10.1016/j.entcs.2012.08.015.

Digital Library

Google Scholar

[8]

W. Jeltsch. Temporal logic with "until", functional reactive programming with processes, and concrete process categories. In Proceedings of the 7th Workshop on Programming Languages Meets Program Verification (PLPV '13), pages 69--78, New York, 2013. ACM. ISBN 978-1-4503-1860-0. 10.1145/2428116.2428128.

Digital Library

Google Scholar

[9]

S. Kobayashi. Monad as modality. Theoretical Computer Science, 175 (1): 29--74, Mar. 1997. ISSN 0304-3975. 10.1016/S0304-3975(96)00169-7.

Digital Library

Google Scholar

[10]

N. R. Krishnaswami and N. Benton. Ultrametric semantics of reactive programs. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS '11), pages 257--266, New York, June 2011. IEEE. ISBN 978-1-4577-0451-2. 10.1109/LICS.2011.38.

Digital Library

Google Scholar

[11]

S. Milius. On iteratable {sic} endofunctors. Electronic Notes in Theoretical Computer Science, 69: 287--304, Feb. 2003. ISSN 1571-0661. 10.1016/S1571-0661(04)80570-X.

Crossref

Google Scholar

Cited By

View all

Jaber GRiba C(2021)Temporal Refinements for Guarded Recursive TypesProgramming Languages and Systems10.1007/978-3-030-72019-3_20(548-578)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_20
Janin D(2018)Spatio-Temporal Domains: An OverviewTheoretical Aspects of Computing – ICTAC 201810.1007/978-3-030-02508-3_13(231-251)Online publication date: 15-Oct-2018
https://doi.org/10.1007/978-3-030-02508-3_13
Jeffrey AHenzinger TMiller D(2014)Functional reactive typesProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603106(1-9)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603106
Show More Cited By

Index Terms

An abstract categorical semantics for functional reactive programming with processes
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Temporal logic with "Until", functional reactive programming with processes, and concrete process categories
PLPV '13: Proceedings of the 7th workshop on Programming languages meets program verification

Recent research has revealed that the "always" and "eventually" operators from temporal logic correspond to the type constructors for behaviors and events from functional reactive programming (FRP). It is furthermore well-known that the "until" ...
Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming

Linear-time temporal logic (LTL) and functional reactive programming (FRP) are related via a Curry-Howard correspondence. Based on this observation, we develop a common categorical semantics for a subset of LTL and its corresponding flavor of FRP. We ...
Fair reactive programming
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Functional Reactive Programming (FRP) models reactive systems with events and signals, which have previously been observed to correspond to the "eventually" and "always" modalities of linear temporal logic (LTL). In this paper, we define a constructive ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

PLPV '14: Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages meets Program Verification

January 2014

66 pages

ISBN:9781450325677

DOI:10.1145/2541568

Program Chairs:
Nils Anders Danielsson
University of Gothenburg, Sweden
,
Bart Jacobs
KU Leuven - University of Leuven, Belgium

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '14

Sponsor:

SIGPLAN

POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 21, 2014

California, San Diego, USA

Acceptance Rates

PLPV '14 Paper Acceptance Rate 5 of 7 submissions, 71%;

Overall Acceptance Rate 18 of 25 submissions, 72%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
126
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Jaber GRiba C(2021)Temporal Refinements for Guarded Recursive TypesProgramming Languages and Systems10.1007/978-3-030-72019-3_20(548-578)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_20
Janin D(2018)Spatio-Temporal Domains: An OverviewTheoretical Aspects of Computing – ICTAC 201810.1007/978-3-030-02508-3_13(231-251)Online publication date: 15-Oct-2018
https://doi.org/10.1007/978-3-030-02508-3_13
Jeffrey AHenzinger TMiller D(2014)Functional reactive typesProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603106(1-9)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603106
Zawawy M(2014)ConNetProceedings of the 2014 14th International Conference on Computational Science and Its Applications10.1109/ICCSA.2014.38(165-170)Online publication date: 30-Jun-2014
https://dl.acm.org/doi/10.1109/ICCSA.2014.38

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Temporal logic with "Until", functional reactive programming with processes, and concrete process categories

Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming

Fair reactive programming