Developers
Stefan Mitsch | 
André Platzer | 
Nathan Fulton |
Contributors
Yong Kiam Tan | 
Andrew Sogokon | 
Brandon Bohrer |
Fabian Immler | 
Katherine Cordwell |
Past Contributors
Jan-David Quesel | 
Marcus Völp | 
Ran Ji |
Power Users
The KeYmaera X developers are incredibly thankful for the helpful feedback on its earlier versions from all the users everywhere, but especially the power users:
Jean-Baptiste Jeannin | 
Yanni Kouskoulas | 
Khalil Ghorbal |
Primary Responsibilities
If you have a question about KeYmaera X, either ask on the KeYmaera X mailing list or directly ask the right person based on the primary responsibilities listed below.
Developers:- Stefan Mitsch: user interface, archive parser, tactic library, tactic tracing and tactic extraction, lemma mechanism, command line interface, HyDRA web service API, tactic task scheduler, Mathematica+SMT interface, lexer, data model and database storage, ModelPlex tactics, C code generator
- André Platzer: prover microkernel, differential dynamic logic parser+printer, unification-based calculus auto-tactics, forward tactics and engine, help documents
- Nathan Fulton: Bellerophon tactic framework, tactic parser, Mathematica interface, HyDRA web service API
- Yong Kiam Tan: differential equation invariant proving, formula simplifier tactics, Pegasus barrier certificate generation
- Brandon Bohrer: proof term generation and parsing, database storage, security
- Andrew Sogokon: Pegasus invariant generator
- Fabian Immler: interval arithmetic proving
- Katherine Cordwell: Contributions to Pegasus linear invariant generator and qualitative abstraction