Guarded recursive datatype constructors
From MaRDI portal
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
- scientific article; zbMATH DE number 3511563 (Why is no real title available?)
- scientific article; zbMATH DE number 615137 (Why is no real title available?)
- scientific article; zbMATH DE number 1942450 (Why is no real title available?)
- scientific article; zbMATH DE number 1948151 (Why is no real title available?)
- scientific article; zbMATH DE number 1953123 (Why is no real title available?)
- scientific article; zbMATH DE number 941396 (Why is no real title available?)
- Regular expression pattern matching for XML
- Types and programing languages
Cited in
(28)- Type-specialized staged programming with process separation
- Functional un\(|\)unparsing
- Strongly typed term representations in Coq
- Safe typing of functional logic programs with opaque patterns and local bindings
- Implicitly heterogeneous multi-stage programming
- Manufacturing datatypes
- Type-safe code transformations in Haskell
- Language-based program verification via expressive types
- Meta-programming with built-in type equality
- Ambivalent types for principal type inference with GADTs
- Programs using syntax with first-class binders
- Refined environment classifiers. Type- and scope-safe code generation with mutable cells
- A reflection on types
- Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
- Size-based termination of higher-order rewriting
- \textsc{OutsideIn(X)}: modular type inference with local assumptions
- Index-stratified types
- Parametricity for nested types and GADTs
- Typed equivalence of effect handlers and delimited control
- Free theorems and runtime type representations
- Characterizing functions mappable over GADTs
- A Compilation Method for Dynamic Typing in ML
- A dependently typed multi-stage calculus
- Generic multiset programming with discrimination-based joins and symbolic Cartesian products
- Deep induction for inductive families
- Transposing G to \(\text{C}^{\sharp}\): expressivity of generalized algebraic data types in an object-oriented language
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Polymorphic typed defunctionalization and concretization
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)
