Danel Ahman

Contact

address: IF 5.32, School of Informatics, 10 Crichton Street, EH8 9AB, Edinburgh, Scotland

e-mail: D.Ahman {ät} ed.ac.uk

office tel: +44 (0)131 650 6787

Education

2012 - … , PhD student, Laboratory for Foundations of Computer Science, University of Edinburgh (Supervisors: Prof. Gordon Plotkin, Prof. Alex Simpson)

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

Institute of Cybernetics, Tallinn (June-September 2011, August 2012)

Active Systems Ltd, Pärnu (Summers 2007 - 2010)

Interests

Academic

Category theory, Type theory, Logic, Notions of computation and algebraic effects, Formal methods and reasoning, Model-based specification and testing

Non-academic

Road cycling, Football, Reading, British comedies, Films, Travelling

Publications

• 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, to appear.
  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 and unpublished drafts

• 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. Algebraic foundations for refinement types in effectful programming languages
  PhD thesis proposal (1st year report), School of Informatics, University of Edinburgh, 2013 (pdf)
• 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

• I am co-organizing Conor McBride's course on Dependently typed metaprogramming (in Agda) with Sam Lindley
• I am co-organizing a reading group on Homotopy Type Theory with James McKinna

Teaching

Logic Programming (School of Informatics, Autumn 2012, Autumn 2013) (LP)

In autumn 2013, I am tutoring one tutorial group and marking students' coursework.

In autumn 2012, I tutored two tutorial groups and marked students' coursework.

Functional Programming (School of Informatics, Autumn 2012, Autumn 2013) (FP)

In autumn 2013, I am tutoring two tutorial groups.

In autumn 2012, I tutored one tutorial group.

Computation and Logic (School of Informatics, Autumn 2013) (CL)

In autumn 2013, I am tutoring one tutorial group.

Language Semantics and Implementation (School of Informatics, Spring 2013) (LSI)

In spring 2013, I tutored one tutorial group.

Object-Oriented Programming (School of Informatics, Spring 2013) (INF1-OP)

In spring 2013, I was a lab demonstrator for one 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.

Talks

• 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)

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

Selection of quotes

• "By three methods we may learn wisdom: First, by reflection, which is noblest; Second, by imitation, which is easiest; and third by experience, which is the bitterest." - Confucius
• "You must be the change you wish to see in the world." - Gandhi
• "The person who reads too much and uses his brain too little will fall into lazy habits of thinking." - Albert Einstein
• "Love is the irresistible desire to be irresistibly desired." - Mark Twain
• "Always forgive your enemies; nothing annoys them so much." - Oscar Wilde
• "Perfection is achieved, not when there is nothing more to add, but when there is nothing left to take away." - Antoine de Saint-Exupery
• "Keep your friends close and your enemies closer." - Sun-Tzu
• "A deadline is negative inspiration. Still, it is better than no inspiration at all." - Rita Mae Brown
• "Nothing is particularly hard if you divide it into small jobs" - Henry Ford
• "Some books are to be tasted, others to be swallowed, and some few to be chewed and digested." - Francis Bacon