[ The Types Forum (announcements only),
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Interactive Theorem Proving
National Institute of Aerospace (Hampton, VA, USA)

The National Institute of Aerospace (NIA), located in Hampton, Virginia, has an 
opening for the position of Research Scientist to work on research and 
development of theorem proving technology for the formal verification of 
autonomous systems. The successful candidate is expected to provide support to 
researchers who are using the Prototype Verification System (PVS) interactive 
theorem prover for the formal verification of autonomous aircraft systems. 
Representative activities may include developing mathematical models, automated 
strategies, tool interfaces, and, in general, advancing the state-of-the-art of 
theorem proving technology through the PVS system.

Required Skills:
• Master’s degree or Ph.D. degree in Computer Science or equivalent.
• Proved experience with higher-order logic.
• Proved experience in functional programming, e.g., Lisp, Scheme, OCaml, ML, 
Haskell, etc.
• Familiar with Unix environment, e.g., Unix, MacOS, Linux, etc.

Desired Skills:
• Experience in interactive theorem proving and proof assistants based on 
higher-order logic, e.g., PVS, Coq, Isabelle, HOL, ACL2, etc.
• Experience in development of verification tools
• Familiar with Common Lisp and the Common Lisp Object System

Interested candidates should apply via NIA’s career opportunities site located 
at www.nianet.org<http://www.nianet.org> under the ‘About NIA’ tab.  Please 
include a letter of introduction, resume, and the names and contact information 
of three current professional references.

If you have any question please contact Sabine Watson 

NIA, located near NASA Langley Research Center in Hampton, Virginia, is a 
non-profit research and graduate education institute created to perform 
aerospace and atmospheric research, develop new technologies for the nation, 
and help inspire the next generation of scientists and engineers.  Additional 
information about NIA and its research programs is available at 
NIA is winner of the 2017 Top 50 Best Non-Profit Companies to work for in the 
NIA is an equal opportunity/affirmative action employer and does not 
discriminate against any applicant for employment or employee because of race, 
color, religion, sex, sexual orientation, gender identity, national origin, age 
disability, protected veteran status, or any other characteristic prohibited 
under Federal, State, or local laws.

Laura Titolo
Research Scientist
National Institute of Aerospace
100 Exploration Way
Hampton, VA 23666
Phone: +1 (757) 325-6905
Fax: +1 (757) 325-6701

National Institute of Aerospace: This e-mail message (including all attachments 
transmitted with it, if any) is intended solely for the use of the addressee 
and may contain company proprietary information. If you are not the person to 
whom this e-mail is addressed, or an employee or agent responsible for 
delivering this message to the person to whom it is addressed, you are hereby 
notified that any dissemination, distribution, copying, or other use of this 
message or its attachments is strictly prohibited. If you have received this
e-mail in error, please notify the sender immediately by e-mail reply, then 
please delete this e-mail, together with any attachments to it, from your 

Reply via email to