Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract)

DOI10.1007/978-3-642-03741-2_9zbMath1239.68025OpenAlexW2113822071MaRDI QIDQ2888481

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

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

Related Items (5)

Undecidability of equality for codata types ⋮ Unnamed Item ⋮ Coalgebras as Types Determined by Their Elimination Rules ⋮ Integrating induction and coinduction via closure operators and proof cycles ⋮ Cubical Agda: A dependently typed programming language with univalence and higher inductive types

Uses Software

• Coq
• Haskell

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Containers: Constructing strictly positive types
• The view from the left
• Indexed containers
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract)