Pinned Repositories
AutoInAgda
An implementation of a first-order auto tactic for Agda, in Agda.
AutoInAgda-ECOSC
Repository for my experimentation project with AutoInAgda
Dissection-thesis
My MSc Thesis on: Verified tail-recursive folds through dissection
FunFlow
Control-flow analysis
HCrawler
A simple webCrawler written in Haskell
Javalette-Compiler
A full-compiler of a C-like language
martin
An interactive programming tutor for Agda
ni-nbe
Noninterference by normalization (by evaluation)
shrdlite
A (very) light version of the program for understanding natural language SHRDLU (http://hci.stanford.edu/winograd/shrdlu/)
wlp-engine
Weakest liberal precondition verifier engine
carlostome's Repositories
carlostome/AutoInAgda
An implementation of a first-order auto tactic for Agda, in Agda.
carlostome/AutoInAgda-ECOSC
Repository for my experimentation project with AutoInAgda
carlostome/Dissection-thesis
My MSc Thesis on: Verified tail-recursive folds through dissection
carlostome/ni-nbe
Noninterference by normalization (by evaluation)
carlostome/agda-stdlib
The Agda standard library
carlostome/agda-steroids
Minimal Prelude fully compatible with agda standard library
carlostome/AutoInAgda-benchmark
carlostome/carlostome.github.io
carlostome/cat
A formalization of category theory in cubical Agda
carlostome/cubical
An experimental library for Cubical Agda
carlostome/dcc-as-reader-monad
carlostome/hnix
A Haskell re-implementation of the Nix expression language
carlostome/home-manager
Manage a user environment using Nix
carlostome/ipl
Agda formalization of Intuitionistic Propositional Logic
carlostome/k
Mechanization of Fitch-style Intuitionistic K
carlostome/latex-biblio
carlostome/latex-myabbreviations
carlostome/latex-myamsthm
carlostome/latex-mycompounds
carlostome/latex-myhyphenation
carlostome/latex-mymacros
LaTex macros
carlostome/latex-mymathpartir
carlostome/latex-mymathtools
carlostome/latex-mystix2
carlostome/latex-mytikz-cd
carlostome/ModalTypeTheory
carlostome/nixpkgs
Nix Packages collection
carlostome/qmk_firmware
Open-source keyboard firmware for Atmel AVR and Arm USB families
carlostome/stgi
A user-centric visual STG implementation to help understand GHC/Haskell's execution model.
carlostome/TypeTopology
Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.