The main task of this position is to implement and maintain proof assistants for dependent type theory as part of the project Constructive Mathematics and Its Synthetic Concepts from Type Theory sponsored by the AFOSR (Air Force Office of Scientific Research). Our current focus is the cooltt project (https://github.com/RedPRL/cooltt/) but we might start other projects depending on the need.
90% Implement and maintain proof assistants for dependent type theory as part of the project Constructive Mathematics and Its Synthetic Concepts from Type Theory sponsored by the AFOSR (Air Force Office of Scientific Research). 10% Attend the project meetings and communicate with other team members on the agreed platforms.
Required Qualifications BA/BS degree required. Two years of work experience in the areas of application/web/systems development with a related BA/BS degree. Four years of work experience in the areas of application/web/systems development with a non-related BA/BS degree. The work experience includes work that was paid and unpaid, as an employee in industry or in any other arrangement. The experience needs to be clear in the CV or resume when applying, or the application may not be forwarded.
You are expected to contribute to the cooltt proof assistant (https://github.com/RedPRL/cooltt/) or similar projects. The following is a detailed breakdown of the necessary skills:
1. Proficiency in OCaml or similar programming languages such as (but not limited to) Standard ML, Haskell, Idris, F#, Scheme, Lisp, or Racket. 2. Prior experience in interactive proof assistants such as (but not limited to) Agda, Lean, or Coq. 3. Proficiency in the Git version control system and experience in communicating with other contributors in open source projects on GitHub or similar websites. 4. The personality and ability to conduct work under remote supervision. 5. The personality and ability to dive deeply into technical details and conduct experiments to assess different possible designs. 6. The personality and ability to maintain open, direct communication and collegial working atmosphere. 7. Bachelor’s Degree (or higher)
Preferred Qualifications 1. Knowledge in homotopy type theory and cubical type theory. 2. Prior experience in making proof checkers or proof assistants. In particular, knowledge of type checking, normalization by evaluation, and elaboration of tactics. 3. Knowledge in OCaml toolchains (dune, opam, etc.), advanced editors (Vim, Emacs, etc.), and continuous integration.
Internal Number: 339220
About University of Minnesota, Twin Cities
The University of Minnesota, founded in the belief that all people are enriched by understanding, is dedicated to the advancement of learning and the search for truth; to the sharing of this knowledge through education for a diverse community; and to the application of this knowledge to benefit the people of the state, the nation, and the world.