rodrigogribeiro Goto Github PK

agda-dtp-examples

agda-small-developments-and-examples

A collection of mostly unrelated Agda programs which I found interesting in some way.

agda-software-foundations

Porting of software foundations book to Agda

agda-tutorial

My solutions to the proposed exercices of a Agda tutorial.

agda-unimath

Univalent mathematics in Agda

ajhc

A fork of jhc.

al-folio

A beautiful Jekyll theme for academics

apostila-discreta

Material para Matemática Discreta

ardlib

assignment01-lexer

astrovim-config

Astrovim config

automata-theory

bcc222-material

bcc244-lecturenotes

Lecture notes for BCC244

beta-eta-coq

Formalization and extraction of a decision procedure for beta-eta equality of simply typed lambda calculus in Coq

bidir

A formalization of a bidirectional typechecker for STLC with booleans

boosting

Transactional boosting for Haskell.

brainfuck

A Brainfuck interpreter written in Agda

coinduction

Being a place where rodrigogribeiro tries to learn conduction

consistency

Formalisation of consistency proofs for minimal propositional logics in Agda and Coq

consistency-coq

Proof of consistency of minimal propositional logics in Coq.

coq-list-zipper

Formalization of list zipper in Coq.

coq-stalin-sort

Formalisation of stalin-sort in Coq

coqcourse

Página de um curso introdutório sobre o assistente de provas Coq.

crud

Using interpreters to automate CRUDs

definitional-ebpf

Towards a definitional interpreter for ebpf

denotational

Having some fun with denotational semantics in Agda

dependent-haskell-playground

Trying to have some fun with GADT, kind promotion, singleton types...

derivatives-racket

Simple implementation of derivatives for regular expressions in racket

developing-dependently-typed-programs-agda

Code for a port of Connor McBride's talk "Developing Dependently Typed Programs in Lego" to Agda.