Let's see how things unfold: reconciling the infinite with the intensional (extended abstract)
DOI10.1007/978-3-642-03741-2_9zbMATH Open1239.68025OpenAlexW2113822071MaRDI QIDQ2888481FDOQ2888481
Authors: Conor McBride
Publication date: 1 June 2012
Published in: Algebra and Coalgebra in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-03741-2_9
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Containers: Constructing strictly positive types
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Title not available (Why is that?)
- The view from the left
- Title not available (Why is that?)
- Universes in type theory. I. Inaccessibles and Mahlo
- Indexed containers
- State dependent IO-monads in type theory
Cited In (8)
- Title not available (Why is that?)
- THE INEFFABLE NATURE OF BEING. IN MEMORIAM: BERNARD D’ESPAGNAT
- Integrating induction and coinduction via closure operators and proof cycles
- Undecidability of equality for codata types
- Copatterns, programming infinite structures by observations
- Coalgebras as types determined by their elimination rules
- Cubical Agda: a dependently typed programming language with univalence and higher inductive types
- CoCaml: functional programming with regular coinductive types
Uses Software
This page was built for publication: Let's see how things unfold: reconciling the infinite with the intensional (extended abstract)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2888481)