# Dependent Types for Multi-Rate Flows in Synchronous Programming

## TL;DR

This paper demonstrates how dependent types in ATS can be used to verify real-time primitives in a synchronous programming language, enabling advanced static checking through automatic code generation.

## Contribution

It introduces a method to encode real-time primitives in Prelude using ATS's dependent and linear types, and modifies the Prelude compiler for automatic ATS code generation.

## Key findings

- Verification of real-time primitives via dependent types in ATS
- Automatic generation of ATS code from Prelude source
- Enhanced static checking capabilities in synchronous programming

## Abstract

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.