rodrigogribeiro/denotational

Stars
1
Language Agda
Created almost 4 years ago
Updated almost 4 years ago

rodrigogribeiro/denotational

rodrigogribeiro

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Having some fun with denotational semantics in Agda

agda-software-foundations

Porting of software foundations book to Agda

unification

Formalisation of a type unification algorithm in Coq proof assistant.

idrisregexp

Regular expression matching in Idris

apostila-discreta

Material para Matemática Discreta

type-theory

Being the materials of type theory course at UFOP

tutoria-bcc222

Materiais da tutoria de BCC222

coqcourse

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

pcc116-2021-2

logic

An adventure on formalising logics using Agda programming language

bcc222-material

mptc

type inference for haskell

regex

tapl-redex

BCC244-lecturenotes

Lecture notes for BCC244

monoid-prover

A reflective tactic for proving monoid equalities in Idris

agda-tutorial

My solutions to the proposed exercices of a Agda tutorial.

generic

Being a place where rodrigogribeiro study generic programming based on universes on dependently typed languages

regexvm

politics

An utility Agda library for politics formalising their speech.

pcc116-agda-lib

Agda library for the course PCC116 - Logics in Computer Science

finite_types

A library for defining types with a finite number of inhabitants in Coq.

simple-vm

A simple VM as a language in racket

coq-stalin-sort

Formalisation of stalin-sort in Coq

propostatese

UDESC-talk-04-2014

Slides e código para palestra na UDESC em 04/2014

PCC102-2021-1

normalization

Formalizing normalization algorithms

expdsl

simple-order

Simple implementation of a lexicographic ordering using Coq module system