
Contact  Education  Internships  Drafts  Publications  Thesises  Extended abstracts  Awards  Community service  Teaching  Talks
Danel Ahman


 I am currently a Postdoctoral Researcher at Inria Paris, working in the Prosecco team with Cătălin Hriţcu on topics related to the F* language.
 My research is in programming language theory, where I am particularly interested in
 dependent types,
 computational effects (in particular algebraic effects and their handlers),
 languages that include both dependent types and computational effects,
 the use of such languages for writing verified software, and
 the (category theoretic) semantics of such languages.
 Address: Prosecco Team, Inria Paris, 2 rue Simone Iff, 75012 Paris, France
 Email: danel {dot} ahman {at} inria {dot} fr
 Skype: danel {underscore} ahman
 Github: danelahman
Education

 2012  2017, PhD in Theoretical Computer Science, LFCS, School of Informatics, University of Edinburgh
 Thesis topic: Fibred Computational Effects (see below)
 Supervisor: Gordon Plotkin
 Examiners: Paul Blain Levy (external) and James Cheney (internal)

 2011  2012, MPhil in Advanced Computer Science (with Distinction), Computer Laboratory, University of Cambridge
 Dissertation topic: Computational effects, algebraic theories and normalization by evaluation (see below)
 Supervisor: Sam Staton

 2007  2010, BSc in Informatics (with Cum Laude), Tallinn University of Technology
Internships
 Microsoft Research, Redmond, WA (May  August 2016)
 Microsoft Research Silicon Valley, Mountain View, CA (September  November 2014)
 Institute of Cybernetics, Tallinn (March  June 2011, June  September 2011, frequent visitor since then)
 Active Systems, Pärnu (Summers 2007  2010)
Drafts
 G. Martínez, D. Ahman, V. Dumitrescu, N. Giannarakis, C. Hawblitzel, C. Hriţcu, M. Narasimhamurthy, Z. Paraskevopoulou, C. PitClaudel, J. Protzenko, T. Ramananandro, A. Rastogi, N. Swamy. MetaF*: Proof Automation with SMT, Tactics, and Metaprograms
arXiv:1803.06547, July 2018. (pdf)
 D. Ahman. Handling Fibred Algebraic Effects
Proc. ACM Program. Lang., v. 2, POPL, article 7, 2018. (doi link , pdf , Agda code)
 D. Ahman, C. Fournet, C. Hriţcu, K. Maillard, A. Rastogi, N. Swamy. Recalling a Witness: Foundations and Applications of Monotonic State
Proc. ACM Program. Lang., v. 2, POPL, article 65, 2018. (doi link , pdf , paper page)
 D. Ahman, T. Uustalu. Taking Updates Seriously
In R. Eramo, M. Johnson, eds., Proc. of 6th Int. Wksh. on Bidirectional Transformations, BX 2017 (Uppsala, April 2017), v. 1827 of CEUR Workshop Proceedings, pp. 5973. CEURWS, 2017. (pdf)
 D. Ahman, C. Hriţcu, K. Maillard, G. Martínez, G. Plotkin, J. Protzenko, A. Rastogi, and N. Swamy. Dijkstra Monads for Free
In A. Gordon, ed., Proc. of 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 (Paris, January 2017), pp. 515529. ACM, 2017. (doi link , pdf , paper page)
 D. Ahman, N. Ghani, G. Plotkin. Dependent Types and Fibred Computational Effects
In B. Jacobs, C. Löding, eds., Proc. of 19th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2016 (Eindhoven, April 2016), v. 9634 of Lect. Notes in Comput. Sci., pp. 3654. Springer, 2016. (doi link , pdf © Springer)
 D. Ahman, T. Uustalu. Directed containers as categories
In R. Atkey, N. Krishnaswami, eds., Proc. of 6th Wksh. on Mathematically Structured Functional Programming, MSFP 2016 (Eindhoven, April 2016), v. 207 of Electron. Proc. in Theor. Comput. Sci., pp. 8998. Open Publishing Assoc., 2016. (doi link , pdf)
 D. Ahman, T. Uustalu. Coalgebraic update lenses
In B. Jacobs, A. Silva, S. Staton, eds., Proc. of 30th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXX (Ithaca, NY, June 2014), Electron. Notes in Theor. Comput. Sci., v. 308, pp. 2548. Elsevier, 2014. (doi link , pdf © Elsevier)
 D. Ahman, T. Uustalu. Update Monads: Cointerpreting Directed Containers
In R. Matthes, A. Schubert, eds., Postproc. of the 19th Meeting "Types for Proofs and Programs", TYPES 2013, Leibniz International Proceedings in Informatics, Schloss Dagstuhl – LeibnizZentrum für Informatik, Dagstuhl Publishing, pp. 123, 2014. (doi link , pdf)
 D. Ahman, S. Staton. Normalization by evaluation and algebraic effects
In D. Kozen, M. Mislove, eds., Proc. of 29th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXIX (New Orleans, LA, June 2013), v. 298 of Electron. Notes in Theor. Comput. Sci., pp. 5169, Elsevier, 2013. (doi link , pdf © Elsevier , Agda code)
 D. Ahman, T. Uustalu. Distributive laws of directed containers
Progress in Informatics, v. 10, pp. 318, 2013. (doi link , pdf)
 D. Ahman, J. Chapman, T. Uustalu. When is a Container a Comonad?
Logical Methods in Computer Science, v. 10, n. 3, article 14, 2014. (doi link , pdf)
Conference version in L. Birkedal, ed., Proc. of 15th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2012 (Tallinn, March 2012), v. 7213 of Lect. Notes in Comput. Sci., pp. 7488, Springer, 2012. (doi link , pdf © Springer , Agda code)
 D. Ahman, M. Kääramees. ConstraintBased Heuristic Online Test Generation from Nondeterministic I/O EFSMs
In Alexander K. Petrenko and Holger Schlingloff, eds., Proc. of 7th Wksh. on ModelBased Testing, MBT 2012 (Tallinn, March 2012), Electron. Proc. in Theor. Comput. Sci., 80, pp. 115–129, Open Publishing Assoc., 2012. (doi link , pdf)
Thesises
 D. Ahman. Fibred Computational Effects
PhD thesis, Laboratory for Foundations of Computer Science (LFCS), School of Informatics, University of Edinburgh, 2017. (pdf , arXiv mirror , abstract in JFP)
 D. Ahman. Computational effects, algebraic theories and normalization by evaluation
MPhil dissertation, Computer Laboratory, University of Cambridge, 2012. (pdf)
Extended abstracts
 D. Ahman, C. Fournet, C. Hritcu, K. Maillard, A. Rastogi, N. Swamy. Recalling a Witness.
Extended abstract presented at the 6th ACM SIGPLAN Workshop on HigherOrder Programming with Effects, HOPE 2017 (Oxford, September 2017)
 D. Ahman. Handling fibred algebraic effects.
Extended abstract presented at the 6th ACM SIGPLAN Workshop on HigherOrder Programming with Effects, HOPE 2017 (Oxford, September 2017)
 D. Ahman, G. Plotkin. Refinement Types for Algebraic Effects
Extended abstract in T. Uustalu, ed., Book of abstracts of the 21th Meeting "Types for Proofs and Programs", TYPES 2015 (Tallinn, May 2015), pp. 1011. Institute of Cybernetics at Tallinn University of Technology, 2015 (pdf)
 D. Ahman, T. Uustalu. From Stateful to Stackful Computation
Extended abstract presented at the 3rd ACM SIGPLAN Workshop on HigherOrder Programming with Effects, HOPE 2014 (Gothenburg, August 2014)
 D. Ahman, T. Uustalu. Coalgebraic update lenses
Extended abstract in H. Herbelin, P. Letouzey and M. Sozeau, eds., Book of abstracts of the 20th Meeting "Types for Proofs and Programs", TYPES 2014 (Paris, May 2014), pp. 1617. Institut Henri Poincaré, 2014 (pdf)
 D. Ahman. Refinement Types and Algebraic Effects
Extended abstract presented at the 2nd ACM SIGPLAN Workshop on HigherOrder Programming with Effects, HOPE 2013 (Boston, MA, September 2013). (pdf) (accompanying slides)
 D. Ahman, T. Uustalu. Update Monads: Cointerpreting Directed Containers
Extended abstract in R. Matthes, ed., Book of abstracts of the 19th Meeting "Types for Proofs and Programs", TYPES 2013, pp. 1617. Institut de Recherche en Informatique de Toulouse, 2013 (pdf) (accompanying slides)
 D. Ahman, T. Uustalu. Distributive laws of directed containers
Extended abstract in L. Schröder, D. Pattinson, eds., Short Contributions of 11th Int. Wksh. on Coalgebraic Methods in Comput. Sci., CMCS '12 (Tallinn, March/April 2012), pp. 13. Inst. of Cybernetics, 2012. (pdf)
Awards and nominations
 2015, PhD scholarship from the Archimedes Foundation and the Estonian Ministry of Education and Research (Scholarship program Kristjan Jaak, for 20152016)
 2013, Institute of Cybernetics paper of the year 2012 (link)
 2013, Travel scholarship to participate at the ICFP 2013 conference (ACM SIGPLAN)
 2013, Supplementary scholarship (Estonian Students Fund in USA, for 20132014)
 2013, Travel scholarship to participate at the MFPS XXIX and LICS 2013 conferences (Scholarship program Kristjan Jaak)
 2012, Supplementary scholarship (Estonian Students Fund in USA, for 20122013)
 2012, PhD scholarship from the University of Edinburgh (Principal's Career Development Scholarship, for 20122015)
 2012, 3rd prize at the Estonian Ministry of Education and Research dissertations competition (MPhil dissertation, link)
 2012, Estonian Academy of Sciences dissertation award (MPhil dissertation, link)
 2012, Google prize for the best research dissertation in MPhil program Advanced Computer Science, Computer Laboratory, University of Cambridge
 2012, Citrix prize for the best student in MPhil program Advanced Computer Science, Computer Laboratory, University of Cambridge
 2012, Graduated with MPhil in Advanced Computer Science from University of Cambridge (with Distinction)
 2012, Nominee for best paper award at the ETAPS 2012 conference
 2010, Estonian President’s recognition of topranking graduates
 2010, Graduated with BSc in Informatics from Tallinn University of Technology (with Cum Laude)
 2008, Tallinn University of Technology Rector's 100 best starting students award
Program committees
 46th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2019 (Lisbon, January 2019)
 7th ACM SIGPLAN Workshop on HigherOrder Programming with Effects, HOPE 2018 (St Louis, September 2018)
 7th Workshop on Mathematically Structured Functional Programming, MSFP 2018 (Oxford, July 2018)
Course and seminar organisation
Media coverage
Teaching
Program verification with F*
Functional Programming (School of Informatics, University of Edinburgh) (FP)
 In autumn 2015, I tutored one tutorial group.
 In autumn 2013, I tutored two tutorial groups.
 In autumn 2012, I tutored one tutorial group.
ObjectOriented Programming (School of Informatics, University of Edinburgh) (INF1OP)
 In spring 2015, I tutored three tutorial groups.
 In spring 2014, I tutored two tutorial groups.
 In spring 2013, I was a lab demonstrator for one group.
Logic Programming (School of Informatics, University of Edinburgh) (LP)
 In autumn 2015, I tutored two tutorial groups.
 In autumn 2013, I tutored one tutorial group and marked students' coursework.
 In autumn 2012, I tutored two tutorial groups and marked students' coursework.
Computation and Logic (School of Informatics, University of Edinburgh) (CL)
 In autumn 2013, I tutored one tutorial group and marked students' coursework.
Language Semantics and Implementation (School of Informatics, University of Edinburgh) (LSI)
 In spring 2013, I tutored one tutorial group.
Logic in Computer Science (Institute of Cybernetics, Tallinn University of Technology) (ITT0040)
 In autumn 2011, I stood in for Prof. Tarmo Uustalu in 2 lectures and 2 practical sessions.
Operating Systems and Network Administrating (Department of Computer Science, Tallinn University of Technology) (ITV0050)
 In spring 2011, I was one of the lecturers in the operating systems and network administering course at the Tallinn University of Technology. I gave talks and practice/exercise sessions on software packaging and package management, filesystems and (remote) access to them, virtual machines and their technology in desktop and server environments.
Talks
 A fibrational view on computational effects
Theory Seminar, University of Ljubljana, 31.05.2018 (slides)
 Embracing monotonicity in F*
Software Science Departmental Seminar, Tallinn University of Technology, 12.02.2018 (slides)
 Embracing monotonicity in F*
ICETCS Seminar, Reykjavík University, 29.01.2018 (slides)
 Leveraging monotonic state in F*
EUTypes 2018 Working Meeting, Radboud University Nijmegen, 23.01.2018 (slides)
 Recalling a Witness: Foundations and Applications of Monotonic State
45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018), 12.01.2018 (slides)
 Handling Fibred Algebraic Effects
45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018), 10.01.2018 (slides)
 A fibrational view on computational effects
LFCS Seminar, University of Edinburgh, 28.11.2017 (abstract , slides)
 Directed containers, what are they good for?
CLAP Scotland, University of Edinburgh, 20.11.2017 (abstract)
 A fibrational view on computational effects
PLS Seminar, IT University of Copenhagen, 13.11.2017
 Recalling a Witness: Foundations and Applications of Monotonic State
6th ACM SIGPLAN Workshop on HigherOrder Programming with Effects (HOPE 2017), 03.09.2017 (slides)
 Handling Fibred Algebraic Effects
6th ACM SIGPLAN Workshop on HigherOrder Programming with Effects (HOPE 2017), 03.09.2017 (slides)
 Recall for free: preorderrespecting state monads in F*
Prosecco Seminar, Inria Paris, 12.04.2017
 Recall for free: preorderrespecting state monads in F*
Programming Languages Interest Group meeting, University of Edinburgh, 13.10.2016 (slides)
 Recall for free: preorderrespecting state monads in F*
EUTypes WG meeting, NOVA University of Lisbon, 5.10.2016 (slides)
 Recall for free: preorderrespecting state monads in F*
End of internship talk, Microsoft Research, Redmond, WA, 15.08.2016
 Dependent Types and Fibred Computational Effects
19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2016), Eindhoven, 04.04.2016 (slides)
 When is a Container a Comonad?
Category Theory Seminar, University of Edinburgh, 16.03.2016
 Dependent Types and Fibred Computational Effects
Logic and Semantics Seminar, University of Cambridge, 22.01.2016 (abstract , slides)
 Dependent types and fibred computational effects
Theory Seminar, University of Dundee, 11.12.2015
 Dependent types and fibred computational effects
EstonianFinnish Logic Meeting, Rakvere, 15.11.2015
 Basic Category Theory for CS graduate students
LFCS PhD Lunch Seminars, 29.10.2015
 Dependent types and fibred computational effects
Scottish Programming Language Seminar, Edinburgh, 21.10.2015 (abstract)
 Dependent types and fibred computational effects
Estonian Computer Science Theory Days, Jõeküla, 3.10.2015 (abstract)
 Dependentlytyped CBPV (and EEC) and its fibred adjunction models
Computer Science Theory Seminar, Institute of Cybernetics, 28.05.2015 (abstract)
 Refinement types for algebraic effects
21st Meeting "Types for Proofs and Programs", 20.05.2015 (slides)
 Refinement types for algebraic effects
LFCS Lab Lunch, University of Edinburgh, 05.05.2015
 Coalgebraic update lenses
Mathematical Foundations for Programming Semantics (MFPS XXX), 12.06.2014
 Update lenses
Programming Languages Interest Group meeting, University of Edinburgh, 6.06.2014
 Basic Category Theory for CS graduate students
LFCS PhD Lunch Seminars, 26.03.2014
 A propositional refinement type system for algebraic effects
Computer Science Theory Seminar, Institute of Cybernetics, 10.03.2014
 Update monads
19th Estonian Winter School in Computer Science, 05.03.2014 (slides)
 A propositional refinement type system for algebraic effects
Programming Languages Interest Group meeting, University of Edinburgh, 27.01.2014
 Refinement Types and Algebraic Effects
2nd ACM SIGPLAN Workshop on HigherOrder Programming with Effects (HOPE 2013), 28.09.2013 (slides)
 An algebraic perspective on behavioral specifications in effectful languages
Programming languages and semantics seminar, Microsoft Research Redmond, 01.07.2013 (slides)
 Normalization by Evaluation and Algebraic Effects
Mathematical Foundations for Programming Semantics (MFPS XXIX), 23.06.2013
 Normalization by Evaluation and Algebraic Effects
LFCS Seminar, University of Edinburgh, 11.06.2013
 Normalization by Evaluation and Algebraic Effects
MSP Group Away Day on Isle of Arran, 05.06.2013
 Update monads: cointerpreting directed containers
19th Meeting "Types for Proofs and Programs", 23.04.2013 (slides)
 Towards refined notions of computation: multisorted algebras and algebraic effects
18th Estonian Winter School in Computer Science, 06.03.2013 (abstract)
 Towards more refined notions of computation: the global state example
Computer Science Theory Seminar, Institute of Cybernetics, 20.12.2012 (abstract , slides)
 Normalization by evaluation for a language with algebraic effects (and their handlers)
Scottish Programming Languages Seminar, University of Strathclyde, 06.12.2012 (slides)
 Computational effects, algebraic theories and normalization by evaluation
Computer Science Theory Seminar, Institute of Cybernetics, 05.07.2012 (abstract)
 Containers, Comonads and Distributive Laws
Semantics Lunch, University of Cambridge, 25.06.2012 (abstract)
 Computational effects, algebraic theories and normalization by evaluation
MPhil project report presentations, University of Cambridge, 29.05.2012, (slides)
 When is a Container a Comonad?
15th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2012), 28.03.2012 (slides)
 When is a Container a Comonad?
Estonian Computer Science Theory Days at Kubija, 29.01.2012 (abstract)
 When is a Container a Comonad?
Lab Lunch, University of Birmingham, 13.12.2011 (abstract)
 When is a Container a Comonad?
Functional Programming Lab Seminars, University of Nottingham, 02.12.2011 (abstract)
 When is a Container a Comonad?
Computer Science Theory Seminar, Institute of Cybernetics, 22.09.2011 (abstract)