Pinned Repositories
agda-software-foundations
Porting of software foundations book to Agda
apostila-discreta
Material para Matemática Discreta
bcc222-material
bcc328
Materiais do curso de compiladores.
coqcourse
Página de um curso introdutório sobre o assistente de provas Coq.
idrisregexp
Regular expression matching in Idris
pcc116-2021-2
tutoria-bcc222
Materiais da tutoria de BCC222
type-theory
Being the materials of type theory course at UFOP
unification
Formalisation of a type unification algorithm in Coq proof assistant.
rodrigogribeiro's Repositories
rodrigogribeiro/unification
Formalisation of a type unification algorithm in Coq proof assistant.
rodrigogribeiro/BCC244-lecturenotes
Lecture notes for BCC244
rodrigogribeiro/regexvm
rodrigogribeiro/coq-stalin-sort
Formalisation of stalin-sort in Coq
rodrigogribeiro/finite_types
A library for defining types with a finite number of inhabitants in Coq.
rodrigogribeiro/politics
An utility Agda library for politics formalising their speech.
rodrigogribeiro/stalin-sort
Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️
rodrigogribeiro/consistency
Formalisation of consistency proofs for minimal propositional logics in Agda and Coq
rodrigogribeiro/consistency-coq
Proof of consistency of minimal propositional logics in Coq.
rodrigogribeiro/crud
Using interpreters to automate CRUDs
rodrigogribeiro/definitional-ebpf
Towards a definitional interpreter for ebpf
rodrigogribeiro/derivatives-racket
Simple implementation of derivatives for regular expressions in racket
rodrigogribeiro/discretalib
Biblioteca de táticas e definições para ensino de lógica e matemática discreta.
rodrigogribeiro/fj-qc
Quickchecking the semantics of Featherweight Java
rodrigogribeiro/gderiv
Simple regular expression matching using derivatives
rodrigogribeiro/LambdaLight
A simple Lambda Calculus Interpreter written in Haskell. Includes all of the elements of an evaluation environment, with support for name bindings.
rodrigogribeiro/list-machine
rodrigogribeiro/logics
rodrigogribeiro/natural-explosion
Proof that if 0 = 1 then all naturals are the same number. All definitions of naturals and equality, even their properties are entirely made directly. No external or library definition was used.
rodrigogribeiro/nbe
Where rodrigogribeiro implements some normalisation by evaluation algorithms
rodrigogribeiro/pandoc-markdown-book-template
A template for creating epub books from markdown using pandoc.
rodrigogribeiro/racket-bf
A simple brainf*ck implementation in racket
rodrigogribeiro/regex-small-step-model
PLT-Redex model for a small-step semantics for regular expression parsing.
rodrigogribeiro/regexvm-1
Papers, codes and proofs about a certified virtual machine-based algorithm for regular expression parsing
rodrigogribeiro/rust-playground
A place to play and learn about Rust.
rodrigogribeiro/stm-model
rodrigogribeiro/stuffs
rodrigogribeiro/thompson
rodrigogribeiro/typedpeg
rodrigogribeiro/verigrep