The following pages link to Types for Proofs and Programs (Q5712312):
Displaying 17 items.
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- Nominal abstraction (Q617715) (← links)
- Cut elimination for a logic with induction and co-induction (Q1948276) (← links)
- Non-well-founded deduction for induction and coinduction (Q2055840) (← links)
- A two-level logic approach to reasoning about computations (Q2392484) (← links)
- Induction, coinduction, and adjoints (Q2842818) (← links)
- (Q3121528) (← links)
- Dual Calculus with Inductive and Coinductive Types (Q3636828) (← links)
- Lexicographic Path Induction (Q3637202) (← links)
- (Q3805882) (← links)
- (Q4365106) (← links)
- (Q4993349) (← links)
- (Q5155663) (← links)
- A case study in programming coinductive proofs: Howe’s method (Q5236557) (← links)
- A Proof Theoretic Approach to Operational Semantics (Q5262970) (← links)
- Focused Inductive Theorem Proving (Q5747767) (← links)
- Least and Greatest Fixed Points in Linear Logic (Q5892168) (← links)