The following pages link to (Q3789101):
Displaying 17 items.
- Using typed lambda calculus to implement formal systems on a machine (Q688571) (← links)
- Theo: An interactive proof development system (Q688727) (← links)
- A framework for proof systems (Q707742) (← links)
- Unification under a mixed prefix (Q1201348) (← links)
- Implementing tactics and tacticals in a higher-order logic programming language (Q1311396) (← links)
- A proof procedure for the logic of hereditary Harrop formulas (Q1311397) (← links)
- Program tactics and logic tactics (Q1380427) (← links)
- The foundation of a generic theorem prover (Q1823013) (← links)
- Higher-order unification revisited: Complete sets of transformations (Q1823936) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- Uniform proofs as a foundation for logic programming (Q2640596) (← links)
- Focusing in Linear Meta-logic (Q3541726) (← links)
- Higher-order unification with dependent function types (Q5055716) (← links)
- Representing proof transformations for program optimization (Q5210798) (← links)
- Implementing type theory in higher order constraint logic programming (Q5236551) (← links)
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic (Q5504659) (← links)
- The practice of logical frameworks (Q5878905) (← links)
