Guarded recursive datatype constructors
From MaRDI portal
Publication:2942928
DOI10.1145/604131.604150zbMATH Open1321.68161OpenAlexW1984514567MaRDI QIDQ2942928FDOQ2942928
Authors: Hongwei Xi, Chiyan Chen, Gang Chen 
Publication date: 11 September 2015
Published in: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/604131.604150
Recommendations
- The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
- Denotational semantics of recursive types in synthetic guarded domain theory
- Programming and reasoning with guarded recursion for coinductive types
- The clocks are ticking: no more delays!: Reduction semantics for type theory with guarded recursion
- Guarded dependent type theory with coinductive types
Cites Work
Cited In (27)
- Safe typing of functional logic programs with opaque patterns and local bindings
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- \textsc{OutsideIn(X)}: modular type inference with local assumptions
- Polymorphic typed defunctionalization and concretization
- Transposing G to \(\text{C}^{\sharp}\): expressivity of generalized algebraic data types in an object-oriented language
- Size-based termination of higher-order rewriting
- Free theorems and runtime type representations
- Characterizing functions mappable over GADTs
- Refined environment classifiers. Type- and scope-safe code generation with mutable cells
- Ambivalent types for principal type inference with GADTs
- A reflection on types
- Implicitly heterogeneous multi-stage programming
- Meta-programming with built-in type equality
- Functional un\(|\)unparsing
- Type-specialized staged programming with process separation
- Title not available (Why is that?)
- Language-based program verification via expressive types
- Index-stratified types
- Manufacturing datatypes
- Strongly typed term representations in Coq
- Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
- A Compilation Method for Dynamic Typing in ML
- Title not available (Why is that?)
- Generic multiset programming with discrimination-based joins and symbolic Cartesian products
- A dependently typed multi-stage calculus
- Type-safe code transformations in Haskell
- Programs using syntax with first-class binders
Uses Software
This page was built for publication: Guarded recursive datatype constructors
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2942928)
