refined-acl2

Refined ACL2: experimental implementation of ACL2-verifiable code with ML modules and Racket macros.

Build status: failed

Authors
Documentation
Tags
Last updatedTuesday, August 15th, 2017 4:59:57pm (UTC)
Ring1
ConflictsNone
Dependencies
Most recent build results
Version Exceptions
VersionSourceChecksum
defaultgithub://github.com/carl-eastlund/refined-acl2/master2e344ad7bcbc5b5a758296a8158dcf9a7f3880bd
Last checkedTuesday, October 17th, 2017 5:12:03am (UTC)
Last editedThursday, September 5th, 2013 12:11:50am (UTC)
Modules
  • refined-acl2/certify.rkt
  • refined-acl2/model/names.rkt
  • refined-acl2/prelude/core/component.rkt
  • refined-acl2/examples/virtual-machine/descriptions.rkt
  • refined-acl2/legacy/type/base.rkt
  • refined-acl2/examples/id-non-dracula/original.rkt
  • refined-acl2/prelude/list-of.rkt
  • refined-acl2/prelude/core/keywords.rkt
  • refined-acl2/model/acl2.rkt
  • refined-acl2/model/api.rkt
  • refined-acl2/examples/id-non-dracula/check.rkt
  • refined-acl2/examples/vm.rkt
  • refined-acl2/prelude.rkt
  • refined-acl2/prelude/base/struct.rkt
  • refined-acl2/examples/generic.rkt
  • refined-acl2/prelude/core/description.rkt
  • refined-acl2/tests/suite/modular.rkt
  • refined-acl2/prelude/core/imported.rkt
  • refined-acl2/tests/suite/atomic.rkt
  • refined-acl2/prelude/type.rkt
  • refined-acl2/core.rkt
  • refined-acl2/prelude/core/expressions.rkt
  • refined-acl2/prelude/base/datatype.rkt
  • refined-acl2/tests/run.rkt
  • refined-acl2/legacy/type/function.rkt
  • refined-acl2/expansion/grammar.rkt
  • refined-acl2/legacy/ref.rkt
  • refined-acl2/expansion/runtime.rkt
  • refined-acl2/examples/sexp.rkt
  • refined-acl2/legacy/type/theorem.rkt
  • refined-acl2/examples/id-non-dracula/fresh.rkt
  • refined-acl2/tests/suite/macro.rkt
  • refined-acl2/base.rkt
  • refined-acl2/tests/harness.rkt
  • refined-acl2/expansion/simplify.rkt
  • refined-acl2/examples/virtual-machine/soundness.rkt
  • refined-acl2/prelude/core/expansion.rkt
  • refined-acl2/examples/ast.rkt
  • refined-acl2/legacy/type/generic.rkt
  • refined-acl2/legacy/type.rkt
  • refined-acl2/proof/static.rkt
  • refined-acl2/primitive.rkt
  • refined-acl2/legacy/api.rkt
  • refined-acl2/prelude/sexp.rkt
  • refined-acl2/legacy/type/field.rkt
  • refined-acl2/legacy/type/description.rkt
  • refined-acl2/legacy/registry.rkt
  • refined-acl2/prelude/base/shorthand.rkt
  • refined-acl2/kernel.rkt
  • refined-acl2/model.rkt
  • refined-acl2/proof/term.rkt
  • refined-acl2/examples/bug.rkt
  • refined-acl2/prelude/base/primitive.rkt
  • refined-acl2/model/data.rkt
  • refined-acl2/prelude/base/mutual.rkt
  • refined-acl2/model/verify.rkt
  • refined-acl2/examples/id-non-dracula/different.rkt
  • refined-acl2/examples/id-non-dracula/identical.rkt
  • refined-acl2/expansion/names.rkt
  • refined-acl2/prelude/core/input-streams.rkt
  • refined-acl2/proof/dynamic.rkt
  • refined-acl2/legacy/check.rkt
  • refined-acl2/prelude/core/atomic.rkt
  • refined-acl2/tests/suite/surface.rkt
  • refined-acl2/expansion/alpha.rkt
  • refined-acl2/legacy/proof.rkt
  • refined-acl2/prelude/base.rkt
  • refined-acl2/prelude/base/match.rkt
  • refined-acl2/prelude/core/support.rkt
  • refined-acl2/legacy/rename.rkt
  • refined-acl2/legacy/type/component.rkt
  • refined-acl2/tests/diff.rkt
  • refined-acl2/model/parse.rkt
  • refined-acl2/model/quote.rkt
  • refined-acl2/model/subst.rkt
  • refined-acl2/legacy/unique.rkt
  • refined-acl2/prelude/set-of.rkt
  • refined-acl2/legacy/type/value.rkt
  • refined-acl2/expansion/paths.rkt
  • refined-acl2/model/proof-term.rkt
  • refined-acl2/model/syntax.rkt
  • refined-acl2/expansion/dependency.rkt
  • refined-acl2/model/unparse.rkt
  • refined-acl2/tests/suite/component.rkt
  • refined-acl2/examples/diss.rkt
  • refined-acl2/main.rkt
  • refined-acl2/prelude/core.rkt