KO
|
EN
gitlite — search
Search
#javascript
#python
#hacktoberfest
#react
#ai
#typescript
#llm
#go
#golang
#android
#machine-learning
#rust
#deep-learning
#linux
agda-gtt
★ 9
Open GitHub ↗
No description available.
Download README (.md)
Explore Similar Repositories
PedestriansDynamics
:
An evacuation of pedestrians in a room
GerberWriter
:
C# .NET Core library for generating RS-274X ("Gerber") files.
indonesian-coreference-resolution-cnn
:
Coreference resolution system for Indonesian text
winutil
:
Windows utility library
SixChessGo
:
:banana: 这是一个六子棋程序，针对一个公共博弈平台写的算法引擎，采用三维空间暴力搜索的方式对局面进行评估并决策
// repository documentation
Was this content helpful?
★ 0
(0 ratings)
Select Rating:
★
★
★
★
★
Submit Feedback
Recent Feedback
×
Download README
Do you want to download the
README.md
file for
agda-gtt
?
Download (.md)
# Guarded Recursion in Agda via Sized Types In type theory, programming and reasoning with possibly non-terminating programs and potentially infinite objects is achieved using coinductive types. Recursively defined programs of these types need to be productive to guarantee the consistency of the type system. Proof assistants such as Agda and Coq traditionally employ strict syntactic productivity checks, which commonly make programming with coinductive types convoluted. One way to overcome this issue is by encoding productivity at the level of types so that the type system forbids the implementation of non-productive corecursive programs. In this paper we compare two different approaches to type-based productivity: guarded recursion and sized types. More specifically, we show how to simulate guarded recursion in Agda using sized types. We formalize the syntax of a simple type theory for guarded recursion, which is a variant of Atkey and McBride’s calculus for productive coprogramming. Then we give a denotational semantics using presheaves over the preorder of sizes. Sized types are fundamentally used to interpret the characteristic features of guarded recursion, notably the fixpoint combinator. Structure of the code: - Prelude.agda: preliminary functions, syntax of GTT and example of streams - Presheaves.agda: definition of presheaves and natural transformations, operations on presheaves - GTT/Structure.agda: Interpretation of types, contexts, terms, substitutions and definitional equalities - GTT/Typeformers.agda: categorical semantics of GTT - Soundness.agda: soundness and consistency of GTT The formalization uses Agda 2.5.4.2 and Agda standard library 0.16 The file Everything.agda contains the whole formalization.
