Developers
Stefan Mitsch | 
André Platzer | 
Yong Kiam Tan |
Contributors
Katherine Cordwell | 
Aditi Kabra |
Past Developers
Nathan Fulton | 
Brandon Bohrer |
Past Contributors
Fabian Immler | 
Jan-David Quesel | 
Andrew Sogokon |
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
- Yong Kiam Tan: differential equation invariant and liveness proving, formula simplifier tactics, Pegasus barrier certificate generation, switched system stability proving.
- Nathan Fulton: Bellerophon tactic framework, tactic parser, Mathematica interface, HyDRA web service API
- 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