Nothing Special   »   [go: up one dir, main page]

Skip to content

A work-in-progress core language for Agda, in Agda

License

Notifications You must be signed in to change notification settings

EwenBC/agda-core

 
 

Repository files navigation

Something is slowly growing here. It is still fragile so better not disturb it, but you may take a look if you'd like.

What is this? Agda Core is, as its name suggests, intended to be a core language for Agda.

Why make a core language for Agda? Because people whose opinion I value were asking for it. Also, implementing a new language from scratch is fun, so there's that.

How is it implemented? Agda Core is implemented in Agda, naturally. It consists of a well-scoped syntax, an environment-based evaluator, a formal definition of the typing and conversion rules, and a derivation-producing type checker.

What can I use it for? First of all, you can appreciate the beauty of the typing rules. Secondly, we plan to link Agda Core to the main Agda system as a backend, so you can double-check its results. Finally, this project is also intended to serve as a demonstration of how to implement a correct-by-construction type checker for dependent types.

About

A work-in-progress core language for Agda, in Agda

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Agda 90.1%
  • Haskell 7.4%
  • Nix 1.9%
  • Other 0.6%