Published July 11, 2025
| Version ICFP-2025-AEC-submission
Software
Open
Artifact for ICFP '25: Effectful Lenses: There and Back with Different Monads
-
1.
Peking University
-
2.
Description
This is the artifact for "Effectful Lenses: There and Back with Different Monads". It contains proofs and examples written in Agda. The code is developed with Agda-2.7.0.1 and agda-stdlib-2.2.
- The file artifact.zip contains the Agda code and pre-generated HTML documentation.
- The file vm.tar.xz contains a QEMU virtual machine with the Agda compiler and the standard library already setup. It also contains a copy of the artifact files for your convenience.
Both archive contains a README.md.
Files
artifact.zip
Files
(610.5 MB)
| Name | Size | Download all |
|---|---|---|
|
md5:8ddbcff51f266591fd1214de6d7a4566
|
1.7 MB | Preview Download |
|
md5:2d026b12894fd445b6c0f427af639fd3
|
608.8 MB | Download |
Additional details
Funding
- National Natural Science Foundation of China
- W2411051
- Fund for Scientific Research
- 3E231241
- China Scholarship Council