Finiteness and rational sequences, constructively

DOI10.1017/S0956796817000041MaRDI QIDQ5372009zbMATH OpenOpenAlexFDO

Authors Tarmo Uustalu, Niccolò Veltri

Publication date 23 October 2017

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0956796817000041

Mathematics Subject Classification ID

Metamathematics of constructive systems (03F50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• On streams that are finitely red
• Types for Proofs and Programs
• A simple canonical representation of rational numbers
• A note on Mathematics of infinity
• Hereditarily finite sets in constructive type theory

Cites work

• A mechanized theory of regular trees in dependent type theory
• Dependently typed programming in Agda
• Free iterative theories: a coalgebraic view
• Fundamental properties of infinite trees
• scientific article; zbMATH DE number 5831413 (Why is no real title available?)
• scientific article; zbMATH DE number 3512082 (Why is no real title available?)
• Investigating streamless sets
• Language constructs for non-well-founded computation
• On streams that are finitely red
• On the algebraic structure of rooted trees
• Regular trees and the free iterative theory
• The existence and construction of free iterative theories
• The Zipper
• Variations on Noetherianness

Cited in

(6)

• It is decidable whether the image of an \(\mathbb N\)-rational sequence has a base
• Concatenation of finite sequences
• On streams that are finitely red
• REASONING ABOUT TRANSFINITE SEQUENCES
• Foundations of regular coinduction
• Comodule representations of second-order functionals

Describes a project that uses

Uses Software

• Agda

This page was built for publication: Finiteness and rational sequences, constructively

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5372009)