scientific article; zbMATH DE number 1424053
From MaRDI portal
Publication:4945244
Recommendations
- Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening
- Alpha-structural induction and recursion for the lambda calculus in constructive type theory
- scientific article; zbMATH DE number 512879
- Partial inductive definitions as type-systems for \(\lambda\)-terms
- A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
Cited in
(46)- Substitution: A formal methods case study using monads and transformations
- Iteration and coiteration schemes for higher-order and nested datatypes
- Confluence of the coinductive \(\lambda\)-calculus
- Nested abstract syntax in Coq
- A formalized general theory of syntax with bindings: extended version
- Rensets and renaming-based recursion for syntax with bindings
- From signatures to monads in \textsf{UniMath}
- Strongly typed term representations in Coq
- Containers: Constructing strictly positive types
- Indexed induction-recursion
- Modelling parallel quantum computing using transactional memory
- Quantum arrows in Haskell
- Turing-Completeness Totally Free
- A mechanized theory of regular trees in dependent type theory
- Partiality, Revisited
- Some Domain Theory and Denotational Semantics in Coq
- Everybody's got to be somewhere
- Heterogeneous substitution systems revisited
- Monotone (co)inductive types and positive fixed-point types
- scientific article; zbMATH DE number 7379288 (Why is no real title available?)
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- A Functional Abstraction of Typed Invocation Contexts
- High-level signatures and initial semantics
- Verifying selective CPS transformation for shift and reset
- Modules over monads and operational semantics (expanded version)
- Indexed containers
- 2-Dimensional Directed Type Theory
- Semantic analysis of normalisation by evaluation for typed lambda calculus
- Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
- Rensets and renaming-based recursion for syntax with bindings extended version
- Map fusion for nested datatypes in intensional type theory
- The formal theory of relative monads
- Towards the complexity analysis of programming language proof methods
- A syntax for mutual inductive families
- Substitution for non-wellfounded syntax with binders through monoidal categories
- Second-order generalised algebraic theories: signatures and first-order semantics
- Structured monads for generic first-order syntax metatheory
- Syntax monads for the working formal metatheorist
- Substitution in non-wellfounded syntax with variable binding
- On model-theoretic strong normalization for truth-table natural deduction
- Modular abstract syntax trees (MAST): substitution tensors with second-class sorts
- Toward model-theoretic consistency verification in a dependently typed encoding of matching logic
- A principled approach to programming with nested types in Haskell
- Explicit substitutions and higher-order syntax
- Type-based termination of generic programs
- Modules over monads and initial semantics
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4945244)
