Skip to Content

ORBI Benchmarks

This page contains benchmarks set out in the paper “The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations” by Felty et al.

Although partially completed, we intend to continue adding more benchmarks to this page.

Equality of Untyped Lambda Calculus

Logoequal-untyped.lf
tm: type. lam: {M: tm -> tm} tm. app: {M1:tm}{M2:tm} tm. aeq: tm -> tm -> type. deq: tm -> tm -> type. ae_a : {M1: tm}{M2: tm}{N1:tm}{N2:tm} {D1:aeq M1 N1}{D2:aeq M2 N2} aeq (app M1 M2) (app N1 N2). ae_l : {M: tm -> tm}{N: tm -> tm} {D: {z:tm} aeq z z -> aeq (M z) (N z)} aeq (lam ([x] M x)) (lam ([x] N x)). de_a : {M1:tm}{M2:tm}{N1:tm}{N2:tm} {D1: deq M1 N1}{D2: deq M2 N2} deq (app M1 M2) (app N1 N2). de_l : {M: tm -> tm}{N: tm -> tm} {D: {z:tm} deq z z -> deq (M z) (N z)} deq (lam ([x] M x)) (lam ([x] N x)). de_s : {M:tm}{N:tm} {D: deq M N} deq N M. de_t : {M1:tm}{M2:tm}{M3:tm} {D1: deq M1 M2} {D2: deq M2 M3} deq M1 M3. de_r : {M:tm} deq M M.
Last updated on