A model of PCF in guarded type theory

DOI10.1016/j.entcs.2015.12.020zbMath1351.68063OpenAlexW2182079433WikidataQ113317721 ScholiaQ113317721MaRDI QIDQ5971407

Lars Birkedal, Marco Paviotti, Rasmus Ejlers Møgelberg

Publication date: 16 December 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2015.12.020

zbMATH Keywords

denotational semanticstype theoryPCFsynthetic domain theoryguarded recursion

Mathematics Subject Classification ID

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

Related Items (3)

Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda ⋮ Denotational semantics of recursive types in synthetic guarded domain theory ⋮ Guarded Dependent Type Theory with Coinductive Types

Uses Software

• Coq

Cites Work

• LCF considered as a programming language
• Programming and Reasoning with Guarded Recursion for Coinductive Types
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Some Domain Theory and Denotational Semantics in Coq
• A very modal model of a modern, major, general type system
• A type theory for productive coprogramming via guarded recursion
• A Model of Countable Nondeterminism in Guarded Type Theory
• Productive coprogramming with guarded recursion
• Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
• General Recursion via Coinductive Types
• Abstract effects and proof-relevant logical relations
• Impredicative Concurrent Abstract Predicates
• Applicative programming with effects

This page was built for publication: A model of PCF in guarded type theory