Skip to content

Mechanized formalization of Implicit resolution in Agda

License

Notifications You must be signed in to change notification settings

ajrouvoet/implicits.agda

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

AGDA checked proof of "Calculus of Implicits" related theorems

Developed for my thesis "Programs for Free: Towards a formalization of Implicit Resolution in Scala". Building on top of earlier work by (Oliveira, Bruno CdS, et al.).

Usage

The code has been compiled against agda 2.4.2.3 and beyond and should be compatible with the latest version of the agda stdlib.

Typechecking

Install the standard library somewhere by cloning it and add the following snippet to your agda libraries file ~/.agda/libraries:

<AGDA_STDLIB_PATH>/standard-library.agda-lib

Typechecking the proofs is as simple as:

make

Browsable docs

This generates the browsable, syntax highlighted source in doc/html/:

make doc

About

Mechanized formalization of Implicit resolution in Agda

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published