Let's see how things unfold: reconciling the infinite with the intensional (extended abstract)

DOI10.1007/978-3-642-03741-2_9MaRDI QIDQ2888481zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18)

Recommendations

• Copatterns, programming infinite structures by observations
• CoCaml: functional programming with regular coinductive types
• General Recursion via Coinductive Types
• scientific article; zbMATH DE number 1942459
• Coinductive Logic Programming and Its Applications

Cites work

• scientific article; zbMATH DE number 1670486 (Why is no real title available?)
• scientific article; zbMATH DE number 426302 (Why is no real title available?)
• scientific article; zbMATH DE number 4047683 (Why is no real title available?)
• scientific article; zbMATH DE number 1952947 (Why is no real title available?)
• scientific article; zbMATH DE number 2247254 (Why is no real title available?)
• Containers: Constructing strictly positive types
• Indexed containers
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• State dependent IO-monads in type theory
• The view from the left
• Universes in type theory. I. Inaccessibles and Mahlo

Cited in

(8)

• scientific article; zbMATH DE number 7407785 (Why is no real title available?)
• THE INEFFABLE NATURE OF BEING. IN MEMORIAM: BERNARD D’ESPAGNAT
• Undecidability of equality for codata types
• Integrating induction and coinduction via closure operators and proof cycles
• 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

Describes a project that uses

Uses Software

• Haskell
• Coq

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)