Developers
Stefan Mitsch | 
André Platzer | 
Nathan Fulton |
Contributors
Yong Kiam Tan | 
Andrew Sogokon | 
Brandon Bohrer |
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, lemma mechanism, command line interface, HyDRA web service API, tactic task scheduler, Mathematica+SMT interface, data model and database storage, ModelPlex tactics, C code generator
- André Platzer: prover core, differential dynamic logic parser+printer, unification-based calculus auto-tactics, forward tactics and engine, help documents
- Nathan Fulton: Bellerophon tactic framework, tactic parser, tactic extraction, lexer, Mathematica interface, HyDRA web service API
- Yong Kiam Tan: differential equation invariant proving, automatic simplifier tactics
- Andrew Sogokon: Pegasus invariant generator
- Brandon Bohrer: proof term generation and parsing, database storage, security