About
Adelfa is a part of The Sparrow Project , led by Prof. Gopalan Nadathur . It is a proof assistant for reasoning about specifications encoded in the Edinburgh Logical Framework [1].
Similar Projects
Some well-known systems which are related to Adelfa are Twelf and Beluga . Discussions of the similarities and differences of these systems can be found in publications.
Adelfa has taken great inspiration from the Abella proof assistant architecturally. Much of the user interactions with the proof assistant are due to the influence of Abella.
Contributors
The logic underlying Adelfa was developed by Gopalan Nadathur and Mary Southern . The logic is described in in [2].
The initial implementation of Adelfa was completed by Mary Southern as part of their Ph.D. work. It is currently developed and maintained by Chase Johnson as a part of his Ph.D. work.
The Adelfa project logo and branding were designed by Sully Dyvad .
References
- [1] Harper, R., Honsell, F., Plotkin, G.: A Framework for Defining Logics. Journal of the ACM. 40, 143–184 (1993). https://doi.org/10.1145/138027.138060.
- [2] Nadathur, G., Southern, M.: A Logic for Reasoning About LF Specifications, (2021). https://doi.org/10.48550/arXiv.2107.00111.