Aleksandar Nanevski

Available identifiers

zbMath Open nanevski.aleksandarMaRDI QIDQ1426867

List of research outcomes

Publication	Date of Publication	Type
Mtac: a monad for typed tactic programming in Coq	2017-10-23	Paper
Contextual modal type theory	2017-07-12	Paper
Specifying and verifying concurrent algorithms with histories and subjectivity	2016-04-26	Paper
Meta-programming with names and necessity	2015-10-07	Paper
Polymorphism and separation in Hoare type theory	2015-08-03	Paper
Structuring the verification of heap-manipulating programs	2015-06-11	Paper
Mtac: a monad for typed tactic programming in Coq	2015-03-30	Paper
Hoare-style reasoning with (algebraic) continuations	2015-03-30	Paper
Ynot: dependent types for imperative programs	2015-03-16	Paper
Automatic generation of staged geometric predicates	2015-03-09	Paper
How to make ad hoc proof automation less ad hoc	2015-03-05	Paper
Subjective auxiliary state for coarse-grained concurrency	2014-11-27	Paper
Communicating state transition systems for fine-grained concurrent resources	2014-04-16	Paper
Modular reasoning about heap paths via effectively propositional formulas	2014-04-10	Paper
How to make ad hoc proof automation less ad hoc	2014-02-27	Paper
Denotation of contextual modal type theory (CMTT): syntax and meta-programming	2013-05-02	Paper
Partiality, state and dependent types	2011-06-17	Paper
Hoare type theory, polymorphism and separation	2008-12-18	Paper
A Realizability Model for Impredicative Hoare Type Theory	2008-04-11	Paper
Abstract Predicates and Mutable ADTs in Hoare Type Theory	2007-09-04	Paper
Staged computation with names and necessity	2005-11-28	Paper
Automatic generation of staged geometric predicates	2004-03-15	Paper
https://portal.mardi4nfdi.de/entity/Q4493213	2000-08-03	Paper

Research outcomes over time

This page was built for person: Aleksandar Nanevski