- Contact
- address: IF 5.32, School of Informatics, 10 Crichton Street, EH8 9AB, Edinburgh, Scotland
- e-mail: D.Ahman {ätt} ed.ac.uk
- office tel: +44 (0)131 650 6787
- Education
- 2012 - … , PhD student^{†}, Laboratory for Foundations of Computer Science (LFCS), University of Edinburgh
Thesis topic: Fibred computational effects in dependently-typed languages
Supervisors: Gordon Plotkin (1st), Ian Stark (2nd), Alex Simpson (ex 2nd)
- Education (past)
- 2011 - 2012 , MPhil in Advanced Computer Science (with Distinction), University of Cambridge (supervisor: Sam Staton)
- 2010 - intermitted , MSc student, Informatics, Tallinn University of Technology
- 2007 - 2010 , BSc in Informatics (with Cum Laude), Tallinn University of Technology (supervisor: Marko Kääramees)
- Internships
- Microsoft Research, Redmond, WA (May-August 2016)
- Microsoft Research Silicon Valley, Mountain View, CA (September-November 2014)
- Institute of Cybernetics, Tallinn (June-September 2011, frequent visitor since 2012)
- Active Systems Ltd, Pärnu (Summers 2007 - 2010)
^{†} My PhD study is financially supported by the University of Edinburgh (Principal Career Development Scholarship, 2012-2015) and by the Archimedes Foundation in collaboration with the Ministry of Education and Research (Estonian National Scholarship Program Kristjan Jaak, 2015-2016).
Interests
- Category theory, type theory, logic, notions of computation and algebraic effects, formal methods and reasoning, model-based specification and -testing.
Publications
- D. Ahman, C. Hriţcu, 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. 515-529. ACM, 2017. (paper page , pdf)
- 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. 36-54. 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. 89-98. 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. 25-48. Elsevier, 2014. (doi link , pdf © Elsevier)
- D. Ahman, T. Uustalu. Update Monads: Cointerpreting Directed Containers
In R. Matthes, A. Schubert, eds., Post-proc. of the 19th Meeting "Types for Proofs and Programs", TYPES 2013, Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, pp. 1--23, 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. 51-69, Elsevier, 2013. (doi link, pdf © Elsevier)
- D. Ahman, T. Uustalu. Distributive laws of directed containers
Progress in Informatics, v. 10, pp. 3-18, 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. 74-88, Springer, 2012. (doi link , pdf © Springer)
- D. Ahman, M. Kääramees. Constraint-Based Heuristic On-line Test Generation from Non-deterministic I/O EFSMs
In Alexander K. Petrenko and Holger Schlingloff, eds., Proc. of 7th Wksh. on Model-Based Testing, MBT 2012 (Tallinn, March 2012), Electron. Proc. in Theor. Comput. Sci., 80, pp. 115–129, Open Publishing Assoc., 2012. (doi link , pdf)
MPhil dissertation
- D. Ahman. Computational effects, algebraic theories and normalization by evaluation
MPhil dissertation, Computer Laboratory, University of Cambridge, 2012. (pdf)
Extended abstracts
- 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. 10-11. 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 Higher-Order 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. 16-17. Institut Henri Poincaré, 2014 (pdf)
- D. Ahman. Refinement Types and Algebraic Effects
Extended abstract presented at the 2nd ACM SIGPLAN Workshop on Higher-Order 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. 16-17. 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. 1-3. Inst. of Cybernetics, 2012. (pdf)
Organization
Talks
- Recall for free: preorder-respecting state monads in F*
Programming Languages Interest Group meeting, University of Edinburgh, 13.10.2016 (slides)
- Recall for free: preorder-respecting state monads in F*
EUTypes WG meeting, NOVA University of Lisbon, 5.10.2016 (slides)
- Recall for free: preorder-respecting 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
Estonian-Finnish 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)
- Dependently-typed 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 Higher-Order Programming with Effects (HOPE), 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), 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)
Teaching
Functional Programming (School of Informatics, Autumn 2012, Autumn 2013) (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.
Object-Oriented Programming (School of Informatics, Spring 2013, Spring 2014, Spring 2015) (INF1-OP)
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, Autumn 2012, Autumn 2013) (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, Autumn 2013) (CL)
In autumn 2013, I tutored one tutorial group and marked students' coursework.
Language Semantics and Implementation (School of Informatics, Spring 2013) (LSI)
In spring 2013, I tutored one tutorial group.
Logic in Computer Science (TUT, Autumn 2011) (ITT0040)
In autumn 2011, I stood in for Prof. T. Uustalu in 2 lectures and 2 practical sessions.
Operating Systems and Network Administrating (TUT, Spring 2011) (ITV0050)
In spring 2011, I was one of the lecturers in the operating systems and network administering course in 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.
Awards and nominations
- 2012, 3rd prize at the Estonian Ministry of Education and Research dissertations competition (link)
- 2012, Estonian Academy of Sciences dissertation award (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 from MPhil in Advanced Computer Science from University of Cambridge with Distinction
- 2012, Nominee for best paper award at ETAPS '12 conference
- 2010, Graduated from BSc in Informatics from Tallinn University of Technology with Cum Laude
- 2008, Tallinn University of Technology Rector's 100 best starting students award