scientific article; zbMATH DE number 1424053
From MaRDI portal
Publication:4945244
zbMath0944.03011MaRDI QIDQ4945244
Bernhard Reus, Thorsten Altenkirch
Publication date: 20 September 2000
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
\(\lambda\)-calculustype theoryinductive typesmonadsimply typed \(\lambda\)-calculusKleisli tripleuntyped \(\lambda\)-termsheterogeneous datatypeinductively defined operatorsubstitution lawswell-founded recursion and induction
Mechanization of proofs and logical operations (03B35) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Combinatory logic and lambda calculus (03B40)
Related Items (33)
Semantic analysis of normalisation by evaluation for typed lambda calculus ⋮ A Functional Abstraction of Typed Invocation Contexts ⋮ Confluence of the coinductive \(\lambda\)-calculus ⋮ A principled approach to programming with nested types in Haskell ⋮ Some Domain Theory and Denotational Semantics in Coq ⋮ Explicit substitutions and higher-order syntax ⋮ Strongly typed term representations in Coq ⋮ Turing-Completeness Totally Free ⋮ A Mechanized Theory of Regular Trees in Dependent Type Theory ⋮ Verifying Selective CPS Transformation for Shift and Reset ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Map fusion for nested datatypes in intensional type theory ⋮ Nested abstract syntax in Coq ⋮ Unnamed Item ⋮ Indexed containers ⋮ Unnamed Item ⋮ Type-based termination of generic programs ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic ⋮ Modules over monads and initial semantics ⋮ 2-Dimensional Directed Type Theory ⋮ Substitution in non-wellfounded syntax with variable binding ⋮ Iteration and coiteration schemes for higher-order and nested datatypes ⋮ Unnamed Item ⋮ High-level signatures and initial semantics ⋮ Modelling Parallel Quantum Computing Using Transactional Memory ⋮ From signatures to monads in \textsf{UniMath} ⋮ Heterogeneous Substitution Systems Revisited ⋮ Containers: Constructing strictly positive types ⋮ Indexed induction-recursion ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs ⋮ Quantum Arrows in Haskell
Uses Software
This page was built for publication:
