Popular repositories Loading

1. hs-to-rocq hs-to-rocq Public

   Convert Haskell source code to Coq source code.

   Rocq Prover 93 11

2. metalib metalib Public

   The Penn Locally Nameless Metatheory Library

   Coq 76 24

3. cis670-16fa cis670-16fa Public

   Advanced Topics in Programming Languages, Penn CIS 670, Fall 2016

   Coq 42 10

4. lngen lngen Public

   Tool for generating Locally Nameless definitions and proofs in Coq, working together with Ott

   Haskell 33 9

5. cis6700-23sp cis6700-23sp Public

   CIS 6700, Spring 2023

   Agda 19 1

6. cbpv-effects-coeffects cbpv-effects-coeffects Public

   Formalization of CBPV extended with effect and coeffect tracking

   Coq 15