scientific article
From MaRDI portal
Publication:3784044
zbMath0643.03010MaRDI QIDQ3784044
Publication date: 1987
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
typed lambda calculusrecursive typeslistsnormalization theoremcategorical type constructorsF-G dialgebras
Specification and verification (program logics, model checking, etc.) (68Q60) Categorical logic, topoi (03G30) Combinatory logic and lambda calculus (03B40) Categories and theories (18C99)
Related Items (43)
Generic recursive lens combinators and their calculation laws ⋮ Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract) ⋮ Bisimulations Generated from Corecursive Equations ⋮ A perspective on service orchestration ⋮ Parametricity of extensionally collapsed term models of polymorphism and their categorical properties ⋮ Classical (co)recursion: Mechanics ⋮ Algebras versus coalgebras ⋮ Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications ⋮ Codatatypes in ML ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A generalization of the concept of sketch ⋮ Unnamed Item ⋮ Friends with Benefits ⋮ Coinduction in Flow: The Later Modality in Fibrations ⋮ Circuits as streams in Coq: Verification of a sequential multiplier ⋮ Categorical ML -- category-theoretic modular programming ⋮ Unnamed Item ⋮ From Algebras and Coalgebras to Dialgebras ⋮ Modularity and Implementation of Mathematical Operational Semantics ⋮ The Recursion Scheme from the Cofree Recursive Comonad ⋮ Termination checking with types ⋮ Kolmogorov Complexity of Categories ⋮ Some Remarks on Type Systems for Course-of-value Recursion ⋮ Iteration and coiteration schemes for higher-order and nested datatypes ⋮ Unnamed Item ⋮ Recursive coalgebras from comonads ⋮ Semantics of constructions. II: The initial algebraic approach ⋮ Least and greatest fixed points in intuitionistic natural deduction ⋮ Undecidability of equality for codata types ⋮ Unnamed Item ⋮ List-arithmetic distributive categories: Locoi ⋮ Structures definable in polymorphism ⋮ Structural induction and coinduction in a fibrational setting ⋮ Relationships between category theory and functional programming with an application ⋮ On the algebraic structure of declarative programming languages ⋮ Two extensions of system F with (co)iteration and primitive (co)recursion principles ⋮ A hidden agenda ⋮ Universal coalgebra: A theory of systems ⋮ Coalgebras as Types Determined by Their Elimination Rules ⋮ The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categorical semantics ⋮ Defining concurrent processes constructively ⋮ An Exercise on Transition Systems
This page was built for publication:
