Denotational semantics of recursive types in synthetic guarded domain theory

Autor: Rasmus Ejlers Møgelberg, Marco Paviotti
Rok vydání: 2016
Předmět:
FOS: Computer and information sciences
Computer Science - Logic in Computer Science
Double recursion
Semantics (computer science)
Computer science
0102 computer and information sciences
02 engineering and technology
computer.software_genre
01 natural sciences
Mutual recursion
Operational semantics
Predicate transformer semantics
Mathematics (miscellaneous)
Denotational semantics
Computer Science::Logic in Computer Science
0202 electrical engineering
electronic engineering
information engineering
Domain theory
0101 mathematics
QA
Mathematics
Soundness
Computer Science - Programming Languages
Recursion
Recursive data type
Simply typed lambda calculus
QA9
Programming language
010102 general mathematics
020207 software engineering
Denotational semantics of the Actor model
Logic in Computer Science (cs.LO)
Computer Science Applications
Type theory
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
010201 computation theory & mathematics
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Computer Science::Programming Languages
computer
Programming Languages (cs.PL)
Zdroj: LICS
Møgelberg, R E & Paviotti, M 2016, Denotational semantics of recursive types in synthetic guarded domain theory . in LICS '16 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science . Association for Computing Machinery, pp. 317-326 . https://doi.org/10.1145/2933575.2934516
Møgelberg, R E & Paviotti, M 2018, ' Denotational semantics of recursive types in synthetic guarded domain theory ', Mathematical Structures in Computer Science . https://doi.org/10.1017/S0960129518000087
ISSN: 0960-1295
DOI: 10.1145/2933575.2934516
Popis: 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 inGuarded Dependent Type Theory(GDTT), we develop denotational semantics for Fixed Point Calculus (FPC), the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types ofGDTT. We prove soundness and computational adequacy of the model inGDTTusing 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.
Databáze: OpenAIRE
Externí odkaz: