Opam Package abella.2.0.7

Package info

opam-nameabella
opam-version2.0.7
synopsisInteractive theorem prover based on lambda-tree syntax
authors
  • Andrew Gacek
  • Yuting Wang
  • Kaustuv Chaudhuri
homepagehttp://abella-prover.org
licenseGPL-3.0-only
deps (3)
revdeps(0)
metas(0)
libraries(0)

Package modules

Package sources

abella

Package files

share/abella/examples/schm-poly/schm_poly_tst.thm
share/abella/examples/schm-poly/schm_poly_tst.sig
share/abella/examples/schm-poly/schm_poly_tst.mod
share/abella/examples/schm-poly
share/abella/examples/programming-languages/poplmark-2a.thm
share/abella/examples/programming-languages/poplmark-2a.sig
share/abella/examples/programming-languages/poplmark-2a.mod
share/abella/examples/programming-languages/poplmark-1a.thm
share/abella/examples/programming-languages/poplmark-1a.sig
share/abella/examples/programming-languages/poplmark-1a.mod
share/abella/examples/programming-languages/pcf.thm
share/abella/examples/programming-languages/pcf.sig
share/abella/examples/programming-languages/pcf.mod
share/abella/examples/programming-languages/howe/subst.thm
share/abella/examples/programming-languages/howe/sim.thm
share/abella/examples/programming-languages/howe/pclf.sig
share/abella/examples/programming-languages/howe/pclf.mod
share/abella/examples/programming-languages/howe/howe.thm
share/abella/examples/programming-languages/howe
share/abella/examples/programming-languages/ees.thm
share/abella/examples/programming-languages/ees.sig
share/abella/examples/programming-languages/ees.mod
share/abella/examples/programming-languages
share/abella/examples/process-calculi/pic_two_level/pic.thm
share/abella/examples/process-calculi/pic_two_level/pic.sig
share/abella/examples/process-calculi/pic_two_level/pic.mod
share/abella/examples/process-calculi/pic_two_level/finite-pic.thm
share/abella/examples/process-calculi/pic_two_level/finite-pic.sig
share/abella/examples/process-calculi/pic_two_level/finite-pic.mod
share/abella/examples/process-calculi/pic_two_level/finite-pic-cong.thm
share/abella/examples/process-calculi/pic_two_level
share/abella/examples/process-calculi/pic_lambda/trans_is_bisimulation.thm
share/abella/examples/process-calculi/pic_lambda/trans.thm
share/abella/examples/process-calculi/pic_lambda/processes_terms.sig
share/abella/examples/process-calculi/pic_lambda/processes_terms.mod
share/abella/examples/process-calculi/pic_lambda/picalc_str_eq_is_bisimulation.thm
share/abella/examples/process-calculi/pic_lambda/picalc.thm
share/abella/examples/process-calculi/pic_lambda/lsc.thm
share/abella/examples/process-calculi/pic_lambda
share/abella/examples/process-calculi/pic/pic_ctx.thm
share/abella/examples/process-calculi/pic/pic_core.thm
share/abella/examples/process-calculi/pic/pic_bisim_examples.thm
share/abella/examples/process-calculi/pic/pic_bisim.thm
share/abella/examples/process-calculi/pic
share/abella/examples/process-calculi/ccs_two_level/ccs.thm
share/abella/examples/process-calculi/ccs_two_level/ccs.sig
share/abella/examples/process-calculi/ccs_two_level/ccs.mod
share/abella/examples/process-calculi/ccs_two_level
share/abella/examples/process-calculi/ccs/ccs_ctx.thm
share/abella/examples/process-calculi/ccs/ccs_core.thm
share/abella/examples/process-calculi/ccs/ccs_context.thm
share/abella/examples/process-calculi/ccs/ccs_bisim_examples_helper.thm
share/abella/examples/process-calculi/ccs/ccs_bisim_examples.thm
share/abella/examples/process-calculi/ccs/ccs_bisim_context_examples.thm
share/abella/examples/process-calculi/ccs/ccs_bisim_context.thm
share/abella/examples/process-calculi/ccs/ccs_bisim.thm
share/abella/examples/process-calculi/ccs
share/abella/examples/process-calculi
share/abella/examples/misc/well-founded.thm
share/abella/examples/misc/umt.thm
share/abella/examples/misc/subst.thm
share/abella/examples/misc/subst.sig
share/abella/examples/misc/subst.mod
share/abella/examples/misc/flex-rigid.thm
share/abella/examples/misc/copy.thm
share/abella/examples/misc/copy.sig
share/abella/examples/misc/copy.mod
share/abella/examples/misc/conat.thm
share/abella/examples/misc/colist.thm
share/abella/examples/misc/cascade.thm
share/abella/examples/misc
share/abella/examples/logic/seq.thm
share/abella/examples/logic/hh_meta.thm
share/abella/examples/logic/focus.thm
share/abella/examples/logic/focus.sig
share/abella/examples/logic/focus.mod
share/abella/examples/logic/equiv.thm
share/abella/examples/logic/equiv.sig
share/abella/examples/logic/equiv.mod
share/abella/examples/logic/cut.thm
share/abella/examples/logic/cut.sig
share/abella/examples/logic/cut.mod
share/abella/examples/logic
share/abella/examples/lambda-calculus/type-uniq/type-uniq.thm
share/abella/examples/lambda-calculus/type-uniq/type-uniq.sig
share/abella/examples/lambda-calculus/type-uniq/type-uniq.mod
share/abella/examples/lambda-calculus/type-uniq/type-uniq-single.thm
share/abella/examples/lambda-calculus/type-uniq/type-uniq-lg.thm
share/abella/examples/lambda-calculus/type-uniq/type-uniq-fresh.thm
share/abella/examples/lambda-calculus/type-uniq
share/abella/examples/lambda-calculus/term-structure/path.thm
share/abella/examples/lambda-calculus/term-structure/path.sig
share/abella/examples/lambda-calculus/term-structure/path.mod
share/abella/examples/lambda-calculus/term-structure/normal.thm
share/abella/examples/lambda-calculus/term-structure/normal.sig
share/abella/examples/lambda-calculus/term-structure/normal.mod
share/abella/examples/lambda-calculus/term-structure/debruijn.thm
share/abella/examples/lambda-calculus/term-structure/debruijn.sig
share/abella/examples/lambda-calculus/term-structure/debruijn.mod
share/abella/examples/lambda-calculus/term-structure
share/abella/examples/lambda-calculus/sred.thm
share/abella/examples/lambda-calculus/sred.sig
share/abella/examples/lambda-calculus/sred.mod
share/abella/examples/lambda-calculus/normalization/stlc-weak-norm.thm
share/abella/examples/lambda-calculus/normalization/stlc-weak-norm.sig
share/abella/examples/lambda-calculus/normalization/stlc-weak-norm.mod
share/abella/examples/lambda-calculus/normalization/stlc-strong-norm.thm
share/abella/examples/lambda-calculus/normalization/stlc-strong-norm.sig
share/abella/examples/lambda-calculus/normalization/stlc-strong-norm.mod
share/abella/examples/lambda-calculus/normalization
share/abella/examples/lambda-calculus/fcurry/fcurry.thm
share/abella/examples/lambda-calculus/fcurry/fcurry.sig
share/abella/examples/lambda-calculus/fcurry/fcurry.mod
share/abella/examples/lambda-calculus/fcurry
share/abella/examples/lambda-calculus/eval.thm
share/abella/examples/lambda-calculus/eval.sig
share/abella/examples/lambda-calculus/eval.mod
share/abella/examples/lambda-calculus/cr.thm
share/abella/examples/lambda-calculus/cr.sig
share/abella/examples/lambda-calculus/cr.mod
share/abella/examples/lambda-calculus
share/abella/examples/higher-order/fsub.thm
share/abella/examples/higher-order/fsub.sig
share/abella/examples/higher-order/fsub.mod
share/abella/examples/higher-order/debruijn_ho.thm
share/abella/examples/higher-order/debruijn_ho.sig
share/abella/examples/higher-order/debruijn_ho.mod
share/abella/examples/higher-order/breduce.thm
share/abella/examples/higher-order/breduce.sig
share/abella/examples/higher-order/breduce.mod
share/abella/examples/higher-order/bred_alt.thm
share/abella/examples/higher-order/bred_alt.sig
share/abella/examples/higher-order/bred_alt.mod
share/abella/examples/higher-order
share/abella/examples/first-order/lists.thm
share/abella/examples/first-order/lists.sig
share/abella/examples/first-order/lists.mod
share/abella/examples/first-order/gcd.thm
share/abella/examples/first-order/gcd.sig
share/abella/examples/first-order/gcd.mod
share/abella/examples/first-order/even-odd.thm
share/abella/examples/first-order/add.thm
share/abella/examples/first-order/add.sig
share/abella/examples/first-order/add.mod
share/abella/examples/first-order/ackermann.thm
share/abella/examples/first-order
share/abella/examples
share/abella/emacs/lprolog-mode.el
share/abella/emacs/abella.el
share/abella/emacs/README
share/abella/emacs
share/abella
bin/abella