Record · corpus.blog/posts/01a0874b-4afb-71be-ad76-849e7eabb30b

Sized types and coinduction in Safe Agda

blog.ielliott.io · published 4 September 2024

A record is what was published and who pointed at it. The text of the post is not held here: read it at the source, or at its Wayback capture.

Read the post at blog.ielliott.io Wayback capture

1blogs citing

First cited: —
Most recent: —
Rank this month: not ranked
Links from this post: 22
Words captured: 5,464

Cited by

Blog

In the post

Date

jesper.sikanda.be

Introduction to Coinduction in Agda Part 1: Coinductive Programming Read at the source ↗

—

Links from this post

Link

Host

https://agda.readthedocs.io/en/latest/language/sized-types.html

agda.readthedocs.io

https://github.com/LightAndLight/agda-safe-sized-types

github.com

https://agda.readthedocs.io/en/v2.7.0/language/coinduction.html

agda.readthedocs.io

https://agda.readthedocs.io/en/latest/language/copatterns.html

agda.readthedocs.io

http://conal.net/papers/language-derivatives/

conal.net

https://agda.readthedocs.io/en/v2.7.0/language/sized-types.html

agda.readthedocs.io

https://agda.readthedocs.io/en/v2.7.0/language/safe-agda.html

agda.readthedocs.io

https://agda.readthedocs.io/en/v2.7.0/language/runtime-irrelevance.html

agda.readthedocs.io

https://agda.readthedocs.io/en/v2.7.0/language/termination-checking.html

agda.readthedocs.io

https://en.wikipedia.org/wiki/Yes_(Unix

en.wikipedia.org

http://conal.net/blog/posts/is-haskell-a-purely-functional-language

conal.net

https://en.wikipedia.org/wiki/Coinduction

en.wikipedia.org

https://github.com/LightAndLight/agda-safe-sized-types/blob/8876b3de679618d352481a69e2e1b8ed48b460e6/src/Codata/SafeSized/Stream/Coalgebra.agda

github.com

https://github.com/agda/agda/labels/infinity-less-than-infinity

github.com

https://ionathan.ch/2021/08/04/sized-types.html

ionathan.ch

https://ncatlab.org/nlab/show/HomePage

ncatlab.org

https://ncatlab.org/nlab/show/Burali-Forti%27s+paradox

ncatlab.org

https://github.com/agda/agda/pull/5354

github.com

https://github.com/agda/agda/issues/1201

github.com

https://github.com/agda/agda/issues/1946

github.com

https://github.com/agda/agda/issues/2820

github.com

https://github.com/agda/agda/issues/3026

github.com