Skip to content

plclub/cbpv-in-agda

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

56 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Effects and Coeffects in Call-By-Push-Value

This repository contains an Agda formalization of Section 2 of "Effects and Coeffects in Call-By-Push-Value".

Everything.agda indicates which files correspond to which subsections of the paper, the paper as well refers to specific theorems in this repository.

This code has been tested with Agda version 2.6.2.2 and standard library version 1.7.1.

About

Formalization of Call-By-Push-Value, augmented with effect tracking

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages