danelahman
Associate Professor of Programming Languages @ University of Tartu
University of TartuTartu
Pinned Repositories
aeff-agda
Agda formalisation of the AEff language
Dep-Mon-Parsing
A simple example of monadic parsing (in the dependently typed setting) discussed in Appendix A of my PhD thesis "Fibred Computational Effects".
Directed-Containers
An Agda formalisation of the theory of directed containers
esp32-fstar
Examples of ESP32 applications written and verified in F*, and extracted to C
haskell-coop
An experimental Haskell library for programming with effectful runners.
higher-order-aeff-agda
Agda formalisation of the AEff language (with higher-order payloads, reinstallable interrupt handlers, and dynamic process creation)
lograc-2022
Git repository for the course Logika v računalništvu
Normalization-By-Evaluation
Formalization of normalization by evaluation for the fine-grain call-by-value language extended with algebraic effect theories
POPL18
An Agda formalisation accompanying the examples given in Section 7 of the paper "Handling fibred algebraic effects".
temporal-resources
Agda formalisation of a core language for temporal resources
danelahman's Repositories
danelahman/haskell-coop
An experimental Haskell library for programming with effectful runners.
danelahman/Normalization-By-Evaluation
Formalization of normalization by evaluation for the fine-grain call-by-value language extended with algebraic effect theories
danelahman/Directed-Containers
An Agda formalisation of the theory of directed containers
danelahman/lograc-2022
Git repository for the course Logika v računalništvu
danelahman/POPL18
An Agda formalisation accompanying the examples given in Section 7 of the paper "Handling fibred algebraic effects".
danelahman/aeff-agda
Agda formalisation of the AEff language
danelahman/Dep-Mon-Parsing
A simple example of monadic parsing (in the dependently typed setting) discussed in Appendix A of my PhD thesis "Fibred Computational Effects".
danelahman/esp32-fstar
Examples of ESP32 applications written and verified in F*, and extracted to C
danelahman/eff-star
danelahman/higher-order-aeff-agda
Agda formalisation of the AEff language (with higher-order payloads, reinstallable interrupt handlers, and dynamic process creation)
danelahman/temporal-resources
Agda formalisation of a core language for temporal resources
danelahman/europroofnet.github.io
Sources of the EuroProofNet web site.
danelahman/formaltt
Formalization of type theory
danelahman/lograc-project-2022
Skeleton project repository for the Logika v računalništvu course
danelahman/MihaPac-Masters
Master project