Skip to content

ikedaisuke/TPPmark2011

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

4 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

README
======

A proof of the TPPmark problem in Agda2, which is a translation in Coq.
The original proof in Coq is written by Jacques Garrigue.

http://staff.aist.go.jp/reynald.affeldt/tpp2011/ucd.html
http://staff.aist.go.jp/reynald.affeldt/tpp2011/garrigue_candy.v

About

A proof of the problem TPP2011, called TPPmark

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published