Position Title: Research Associate
Department/Unit: Mathematics & Statistics, Dalhousie University
Research Project: Dependent type theory for verified quantum software
Location: Halifax, NS
Position Type: Term
Duration of Contract (if applicable): 2 years
Employment Type: Full Time
Full-time Equivalency (FTE) 1.0
Salary: $37,050 – $50,000 per annum (37.5 hours per week)
About the Organization:
The “Dependent Type Theory for Verified Quantum Software” research project is within the Department of Mathematics and Statistics at Dalhousie University and involves the design, semantics, and meta-theory of a functional programming language for quantum computing and using the language to investigate questions in quantum information theory.
Job Summary:
Reporting to the Principal Investigator, the Research Associate will work on a project entitled “Dependent type theory for verified quantum software” and related projects. The Research Associate will participate in the design of a type-safe functional quantum programming language and will be involved in the design, semantics, and meta-theory of a functional programming language for quantum computing and using the language to investigate questions in quantum information theory.
Key Responsibilities:
- Apply methods of category theory and formal logic to the design of a type-safe functional quantum programming language.
- Use orthomodular logic, complete partial orders, and quantized versions of set theory in the development of a formal semantics and other meta-theory of the language.
- Investigate connections between quantum sets, quantum cpos, and quantum programming language design.
- Interact with team members at Dalhousie University in support of the research project.
- Travel to attend site visits, program workshops, or for collaborations as directed.
- Publish research results in appropriate journals and other recognized media.
Note:
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 and will be required to provide proof of full vaccination through Campus Check, or may seek an accommodation from Dalhousie’s vaccine requirements on grounds protected under provincial human rights legislation. Please visit the Campus Check website for more information.
Qualifications:
Ph.D. in Mathematics with a minimum of five years of related research experience in category theory, formal logic, and quantum computing. Must possess a strong background in dependent type theory and the categorical semantics of quantum programming languages. Experience in quantum domain theory, orthomodular logic, quantum posets, and variational quantum programming is also required.
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: https://dal.peopleadmin.ca/postings/9310
We thank all applicants for their interest, however, only candidates selected for an interview will be contacted.
Diversity Statement:
Dalhousie University is committed to fostering a collegial culture grounded in diversity and inclusiveness. The university encourages applications from Indigenous persons, persons with a disability, racially visible persons, women, persons of a minority sexual orientation and/or gender identity, and all candidates who would contribute to the diversity of our community. For more information, please visit www.dal.ca/hiringfordiversity.