amintimany
I am an assistant professor of computer science in the logic and semantics research group at Aarhus University.
Aarhus UniversityAarhus, Denmark
amintimany's Stars
Homebrew/brew
🍺 The missing package manager for macOS (or Linux)
Homebrew/homebrew-core
🍻 Default formulae for the missing package manager for macOS (or Linux)
ocaml/ocaml
The core OCaml system: compilers, runtime system, base libraries
coq/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
FStarLang/FStar
A Proof-oriented Programming Language
HoTT/Coq-HoTT
A Coq library for Homotopy Type Theory
UniMath/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
AndrasKovacs/elaboration-zoo
Minimal implementations for dependent type checking and elaboration
math-comp/math-comp
Mathematical Components
ProofGeneral/PG
This repo is the new home of Proof General
verifast/verifast
Research prototype tool for modular formal verification of C and Java programs
RedPRL/redtt
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
coq-community/math-classes
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters]
coq/opam
Archive for all Coq related OPAM packages organized in various repositories
clarkgrubb/latex-input
Enter Unicode characters using LaTeX notation
coq-community/manifesto
Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.
coq-community/autosubst
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
wilbowma/cic-redex
A Redex model of CIC as specified in Chapter 4 of the Coq reference manual.
CoqHott/coq-forcing
A plugin for Coq that implements the call-by-name forcing translation