Denotational semantics of recursive types in synthetic guarded domain theory

DOI10.1145/2933575.2934516MaRDI QIDQ4635887zbMATH OpenOpenAlexFDO

Authors Rasmus Ejlers Møgelberg, Marco Paviotti

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1805.00289, https://kar.kent.ac.uk/69685/1/mscs-fpc.pdf

zbMATH Keywords

type theorydenotational semanticsrecursive typessynthetic domain theoryguarded recursion

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Abstract: Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques. Working in Guarded Dependent Type Theory (GDTT), we develop denotational semantics for FPC, the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types of GDTT. We prove soundness and computational adequacy of the model in GDTT using a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.

Recommendations

• Denotational semantics of recursive types in synthetic guarded domain theory
• Denotational semantics for guarded dependent type theory
• scientific article; zbMATH DE number 1377611
• Programming and reasoning with guarded recursion for coinductive types
• An operational domain-theoretic treatment of recursive types
• An operational domain-theoretic treatment of recursive types
• Guarded computational type theory
• Type inference with recursive types: Syntax and semantics
• A type theory for productive coprogramming via guarded recursion
• Denotational semantics for intuitionistic type theory using a hierarchy of domains with totality

Cited in

(10)

• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Denotational semantics of recursive types in synthetic guarded domain theory
• Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
• Guarded recursive datatype constructors
• The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
• A model of PCF in guarded type theory
• Two guarded recursive powerdomains for applicative simulation
• Denotational semantics for guarded dependent type theory
• Intensional type theory with guarded recursive types qua fixed points on universes
• Codifying guarded definitions with recursive schemes

This page was built for publication: Denotational semantics of recursive types in synthetic guarded domain theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635887)