Теория темпоральных типов: Теоретико-топосный подход к системам и поведению

В этой книге представлена теория временных типов, первая в своем роде, насколько нам известно. Она основана на стандартном ядре и поэтому может быть формализована с помощью помощника по доказательству, такого как COQ или LEAN, путем добавления ряда аксиом. Хорошо известные темпоральные логики, такие как линейная и метрическая темпоральная логика (LTL и MTL), встроены в логику теории темпоральных типов. Типы в этой теории представляют собой «типы поведения». Язык достаточно богат, чтобы позволить определять произвольные гибридные динамические системы, которые представляют собой смесь непрерывных динамик — как описывается дифференциальными уравнениями — и дискретными скачками. В частности, производная непрерывной вещественнозначной функции внутренне определена. Построена семантика теории временных типов в топосах пучков на трансляционно-инвариантном частном стандартной интервальной области. Фактически, теория областей играет повторяющуюся роль, как в семантике, так и в теории типов.