amintimany
I am an assistant professor of computer science in the logic and semantics research group at Aarhus University.
Aarhus UniversityAarhus, Denmark
Pinned Repositories
Categories
A formalization of category theory in the Coq proof assistant.
Categories-HoTT
The HoTT version of Categories.
CTDT
Category-theoretic domain theory.
F_mu_ref_conc_sub
monotone
NbE
Normalization by Evaluation for STLC
opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
OPLSS
UniverseComparator
A tool to compare universe levels in Coq.
amintimany's Repositories
amintimany/Categories
A formalization of category theory in the Coq proof assistant.
amintimany/NbE
Normalization by Evaluation for STLC
amintimany/OPLSS
amintimany/F_mu_ref_conc_sub
amintimany/monotone
amintimany/.doom.d
amintimany/.emacs.d
My .emacs.d folder
amintimany/atomic-block
amintimany/autosubst
Automation for de Bruijn syntax and substitution in Coq
amintimany/column-enforce-mode
Highlight text that extends beyond a certain column. Can be used to enforce 80 column rule (well more like suggest, not enforce)
amintimany/company-coq
IDE extensions for Proof General's Coq mode
amintimany/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.
amintimany/CSrankings
A web app for ranking computer science departments according to their research output in selective venues, and for finding active faculty across a wide range of areas.
amintimany/DRADS19
amintimany/homebrew-core
:beers: Core formulae for the Homebrew package manager
amintimany/iris
My personal copy of iris(https://gitlab.mpi-sws.org/FP/iris-coq.git)
amintimany/iris-io
amintimany/iris-logrel
Logical relations in iris.
amintimany/iris-logrel-notes
amintimany/iris-my-examples
amintimany/iris-spanning-tree
Verification of a concurrent in-place spanning tree algorithm in Iris
amintimany/iris-with-logrel-backup
My copy of iris development
amintimany/prezto
The configuration framework for Zsh
amintimany/robustsafety
amintimany/setcoq
A simple way to manage multiple versions of Coq
amintimany/short-logrel-in-coq
amintimany/short-logrel-notes
amintimany/Types17
amintimany/verifast
Research prototype tool for modular formal verification of C and Java programs
amintimany/x64emu