Coalgebras in functional programming and type theory
From MaRDI portal
Publication:639643
DOI10.1016/j.tcs.2011.04.024zbMath1225.68057OpenAlexW2020914843MaRDI QIDQ639643
Publication date: 22 September 2011
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2011.04.024
Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Abstract data types; algebraic specification (68Q65)
Related Items (2)
Kripke semantics for higher-order type theory applied to constraint logic programming languages ⋮ Bisimulation proof methods in a path-based specification language for polynomial coalgebras
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Notions of computation and monads
- Algebra and coalgebra in computer science. Third international conference, CALCO 2009, Udine, Italy, September 7--10, 2009. Proceedings
- Lectures on the Curry-Howard isomorphism
- A calculus of communicating systems
- Algebraically compact functors
- Structural induction and coinduction in a fibrational setting
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory
- A constructive approach to nonstandard analysis
- Types for proofs and programs. International Workshop TYPES '94, Båstad, Sweden, June 6-10, 1994. Selected papers
- A fixpoint theorem for complete categories
- Containers: Constructing strictly positive types
- Continuous Functions on Final Coalgebras
- Observational Coalgebras and Complete Sets of Co-operations
- Comonadic Notions of Computation
- Circular Coinduction: A Proof Theoretical Foundation
- Relating Coalgebraic Notions of Bisimulation
- Bisimulations Generated from Corecursive Equations
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Representations of Stream Processors Using Nested Fixed Points
- Subtyping, Declaratively
- Computation by Prophecy
- Behavioural Differential Equations and Coinduction for Binary Trees
- Well-Definedness of Streams by Termination
- Dependently Typed Programming in Agda
- The independence of Peano's fourth axiom from Martin-Löf's type theory without universes
- On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces
- A note on Mathematics of infinity
- Setoids in type theory
- A coinductive calculus of streams
- The view from the left
- A final coalgebra theorem
- Functional pearl
- General Recursion via Coinductive Types
- Origins of bisimulation and coinduction
- Productivity of Stream Definitions
- Equality of streams is a Π0 over 2-complete problem
- Modelling general recursion in type theory
- Programming in Haskell
This page was built for publication: Coalgebras in functional programming and type theory
