Functional Compiler Engineer
Runtime Verification Inc. is a technology company headquartered in Urbana, Illinois with staff spread across the globe. We provide testing and verification services to public and private companies in the embedded and blockchain domains. In the latter we work with infrastructure builders as well as companies building products and providing services supported and/or powered by said infrastructure.
Company mission
Our mission is to support and scale accessible, trustworthy computing. We accomplish this by generating correct-by-construction implementations and tools automatically, from their specifications. One of our unique technologies is K, a semantic framework for design, implementation and formal reasoning. It allows language designers to formally define their language using an intuitive and attractive notation, and generate for free the implementations and the analysis tools for that defined language.
Job description
Runtime Verification Inc (RV) is looking for a Functional Compiler Engineer to contribute to the K framework project. The ideal candidate has a strong programming background and knowledge about compilers for imperative and functional programming languages. The successful hire will show initiative and lead the maintenance of our internal compiler technologies. The selected individual will be responsible for the following:
Maintain a compiler developed by RV for a functional programming language, and strategically identify ways to improve the scalability, performance, and reliability of the compiler.
Design and extend the K framework language with ideas from the term rewriting and functional programming paradigms.
Maintain a Java and C++ codebase that parses, compiles, and interprets programs written in this language by the many semantics engineers at RV.
What we offer
Must have
B.S. in software engineering or equivalent.
5+ years of industry experience writing code in a functional programming language or a term rewriting language.
A history of development that includes at least one accepted patch into the compiler of a functional or term rewriting programming language.
Nice to have
Industry experience writing Java or C++ code.
Experience as a maintainer of an open source compiler.
nowledge of formal methods, mathematical logic, or term rewriting.
Familiarity with SMTLIB technology.
Experience with LLVM and Clang.
Knowledge of Flex/Bison.
What’s in it for you?
Opportunity to work at the forefront of programming language design and verification.
Casual work environment with flexible work hours