Research Associate

DALHOUSIE UNIVERSITY, Mathematics & Statistics

Position Title: Research Associate

Department/Unit: Mathematics & Statistics

Research Project: Dependent Type Theory for Verified Quantum Software

Location: Halifax

Position Type: Term

Duration of Contract (if applicable): 2-year term

Employment Type: Full Time

Full-time Equivalency (FTE): 1.0

Unit Full-time Hours: 37.5 hours/week

Salary: $37,050 – $50,000 per annum (37.5 hours per week)

About the Organization:

The Department of Mathematics and Statistics at Dalhousie University is a research-intensive department with 32 faculty members and numerous postdocs and graduate students. The Research Associate will work on a research project entitled “Dependent Type Theory for Verified Quantum Software.”

Job Summary:

Reporting to the Principal Investigator, the Research Associate will be responsible for the design, semantics, and meta-theory of a functional programming language for quantum computing and use the language to investigate questions in quantum information theory.

Key Responsibilities:

  • Apply methods of type theory and lambda calculus to the design and implementation of a type-safe functional quantum programming language.

  • Use category theory, modal logic, and fibrations in the development of formal semantics and other meta-theory of the language.

  • Investigate the use of dependently typed lambda encodings in quantum programming language design.

  • Interact with team members at Dalhousie University.

  • Travel to attend site visits, program workshops, or for collaborations as directed.

  • Publish research results in appropriate journals and other recognized media.


National and international travel will be required several times a year.

Due to operational requirements, the successful applicant is required to work in-person on campus.

Dalhousie’s vaccine mandate has been suspended at this time, and employees no longer need to provide proof of full vaccination. However, health and safety risks to our community will continue to be monitored and a vaccine mandate may be reinstated if necessary.

Required Qualifications:

  • Ph.D. in Mathematics or Computer Science with a minimum of 5 years of related research experience in dependent type theory and lambda calculus.

  • Experience in the design and implementation of quantum programming languages, dependently typed lambda encodings, and the categorical semantics of quantum programming languages.

Additional Information:

Dalhousie University supports a healthy and balanced lifestyle. Our total compensation package includes a voluntary RRSP, health and dental plans and an employee and family assistance program.

Application Consideration:

All qualified candidates are encouraged to apply; however, Canadians and Permanent Residents will be given priority.

To apply you must submit you application via:

We thank all applicants for their interest, however, only candidates selected for an interview will be contacted.

Diversity Statement:

Dalhousie University commits to achieving inclusive excellence through continually championing equity, diversity, inclusion, and accessibility. The university encourages applications from Indigenous persons (especially Mi’kmaq), persons of Black/African descent (especially African Nova Scotians), and members of other racialized groups, persons with disabilities, women, persons identifying as members of 2SLGBTQ+ communities, and all candidates who would contribute to the diversity of our community. For more information, please visit