About

Adelfa is a part of The Sparrow Project, led by Prof. Gopalan Nadathur. It is a proof assistant for the LF logical framework.

Similar Projects

LF is a well-studied logical framework, and there are many proof assistants that are built on top of it. Some of the more well-known ones 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 the paper “A logic for reasoning about LF specifications”.

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.