XDOC Link Check

This is a single web page with the collected external links from your XDOC topics. The purpose of this page is to serve as easy way to run an off-the-shelf link checking program such as. There are any number of link checking programs. You might try:

• (Firefox) The LinkChecker Addon seems very nice; it just goes through the page you're viewing and turns good links green.
• (Perl) The W3C::LinkChecker Perl module comes with a command-line checklink program. Installation was just cpanm W3C::LinkChecker, and running it was just checklink linkcheck.html. Unfortunately it respects robots.txt, so it fails to verify many links.
• (Ruby) Rawler was easy to install with gem install rawler. It couldn't process a local file, so I had to copy my linkcheck.html file to the web server and then run rawler http://.../linkcheck.html. Aside from not following FTP links, it seemed to work well.

There are way more programs than this that check links, so if you can't easily install the above or don't like them, you might try your operating system's package manager.

Links From Each Topic

External links from ACL2____TOP

• http://en.wikipedia.org/wiki/Formal_verification
• http://www.cs.utexas.edu/users/moore/acl2/
• https://github.com/acl2/
• https://github.com/acl2/acl2/tree/master/books

External links from ACL2____SOFTWARE-VERIFICATION

• http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html

External links from ACL2____HARDWARE-VERIFICATION

• http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html

External links from ACL2____BOOLEAN-REASONING

• http://dx.doi.org/10.1007/978-3-642-14052-5_30
• http://dx.doi.org/10.4204/EPTCS.114.8
• http://dx.doi.org/10.4204/EPTCS.70.7
• http://en.wikipedia.org/wiki/And-inverter_graph
• http://en.wikipedia.org/wiki/Binary_decision_diagram
• http://en.wikipedia.org/wiki/Boolean_function
• http://en.wikipedia.org/wiki/Boolean_satisfiability_problem
• http://en.wikipedia.org/wiki/Conjunctive_normal_form
• http://en.wikipedia.org/wiki/Formal_equivalence_checking
• http://en.wikipedia.org/wiki/Model_checking
• http://www.eecs.berkeley.edu/~alanmi/abc/

External links from STOBJS____STOBJ-UPDATER-INDEPENDENCE

• https://plato.stanford.edu/entries/frame-problem/

External links from ACL2____AIG

• http://dx.doi.org/10.4204/EPTCS.114.8
• http://en.wikipedia.org/wiki/And-inverter_graph

External links from ACL2____AIG-RANDOM-SIM

• http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.66.3434

External links from ACL2____BDDIFY

• http://dx.doi.org/10.1007/978-3-642-14052-5_30
• https://www.cs.utexas.edu/users/kaufmann/itp-2010/session6/swords-itp.pdf

External links from ACL2____ESIM

• http://dx.doi.org/10.1007/978-3-642-02658-4_28

External links from ACL2____KESTREL-BOOKS

• http://www.kestrel.edu
• images/res/kestrel-images/kestrel-logo.png

External links from ZCASH____ZCASH

• https://github.com/zcash/zips/blob/master/protocol/protocol.pdf
• https://z.cash

External links from YUL____YUL

• https://docs.soliditylang.org/en/latest/
• https://docs.soliditylang.org/en/latest/yul.html
• https://ethereum.org

External links from YUL____UBYTE16-TO-UTF8

• https://en.wikipedia.org/wiki/UTF-8

External links from YUL____PARSE-VARIABLE-DECLARATION

• https://docs.soliditylang.org/en/v0.8.10/grammar.html#a4.SolidityParser.yulAssignment
• https://docs.soliditylang.org/en/v0.8.10/grammar.html#a4.SolidityParser.yulVariableDeclaration

External links from TREESET____IMPLEMENTATION

• https://en.wikipedia.org/wiki/Treap
• https://www.cs.cmu.edu/~scandal/papers/treaps-spaa98.pdf

External links from TREESET____HEAP_C3

• https://en.wikipedia.org/wiki/Avalanche_effect

External links from TREESET____JENKINS-HASH

• https://burtleburtle.net/bob/hash/doobs.html
• https://en.wikipedia.org/wiki/Jenkins_hash_function#one_at_a_time

External links from SOLIDITY____SOLIDITY

• https://ethereum.org
• https://solidity.readthedocs.io/en/v0.7.0/index.html
• https://solidity.readthedocs.io/en/v0.7.0/types.html

External links from SOLIDITY____VALUES

• https://solidity.readthedocs.io/en/v0.7.0/types.html

External links from SOLIDITY____UINT-SHR

• https://solidity.readthedocs.io/en/v0.7.0/types.html#shifts

External links from SOLIDITY____UINT-SHL

• https://solidity.readthedocs.io/en/v0.7.0/types.html#shifts

External links from SOLIDITY____INT-MOD

• https://solidity.readthedocs.io/en/v0.7.0/types.html#modulo

External links from SOLIDITY____INT-DIV

• https://solidity.readthedocs.io/en/v0.7.0/types.html#division

External links from SOLIDITY____UINT-MOD

• https://solidity.readthedocs.io/en/v0.7.0/types.html#modulo

External links from SOLIDITY____UINT-DIV

• https://solidity.readthedocs.io/en/v0.7.0/types.html#division

External links from SOLIDITY____INTEGER-OPERATIONS

• https://solidity.readthedocs.io/en/v0.7.0/types.html#exponentiation
• https://solidity.readthedocs.io/en/v0.7.0/types.html#implicit-conversions
• https://solidity.readthedocs.io/en/v0.7.0/types.html#integers
• https://solidity.readthedocs.io/en/v0.7.0/types.html#shifts

External links from SOLIDITY____INTEGER-VALUES

• https://solidity.readthedocs.io/en/v0.7.0/types.html#integers

External links from SOLIDITY____BOOLEAN-OPERATIONS

• https://solidity.readthedocs.io/en/v0.7.0/types.html#booleans

External links from SOLIDITY____BOOLEAN-VALUES

• https://solidity.readthedocs.io/en/v0.7.0/types.html#booleans

External links from SOFT____SOFT-FUTURE-WORK

• http://eptcs.web.cse.unsw.edu.au/paper.cgi?ACL22015.3

External links from SOFT____SOFT

• http://eptcs.web.cse.unsw.edu.au/paper.cgi?ACL22015.3
• http://www.cs.utexas.edu/users/moore/acl2/workshop-2015/program.html

External links from SIMPL-IMP____IMP-LANGUAGE

• http://concrete-semantics.org
• https://softwarefoundations.cis.upenn.edu/current/lf-current/Imp.html
• https://www.cs.cmu.edu/~mfredrik/15414/lectures/10-semantics.pdf

External links from RISCV____RISCV

• https://riscv.org
• https://riscv.org/technical/specifications/

External links from JSON____JSON

• http://www.json.org
• https://tools.ietf.org/html/rfc8259
• https://www.ecma-international.org/publications-and-standards/standards/ecma-404
• https://www.iso.org/standard/71616.html
• https://www.rfc-editor.org/errata/rfc8259

External links from JAVA____JAVA

• https://docs.oracle.com/en/java/javase/21/docs/api
• https://docs.oracle.com/javase/specs/jls/se21/html
• https://docs.oracle.com/javase/specs/jvms/se21/html

External links from JAVA____ATJ-TUTORIAL-NATIVE-FUNCTIONS

• https://docs.oracle.com/javase/10/docs/specs/jni

External links from JAVA____ATJ-TUTORIAL-ACL2-ENVIRONMENT

• images/res/kestrel-java-atj-images/package-classes.png

External links from JAVA____ATJ-TUTORIAL-ACL2-TERMS

• https://docs.oracle.com/javase/10/docs/specs/jni
• images/res/kestrel-java-atj-images/term-classes.png

External links from JAVA____ATJ-TUTORIAL-DEEP

• images/res/kestrel-java-atj-images/aij-api.png
• images/res/kestrel-java-atj-images/atj-aij-api.png

External links from JAVA____ATJ-TUTORIAL-ACL2-VALUES

• https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node18.html
• images/res/kestrel-java-atj-images/value-classes.png
• images/res/kestrel-java-atj-images/values.png

External links from JAVA____ATJ-TUTORIAL-SIMPLIFIED-UML

• http://uml.org

External links from JAVA____ATJ-TUTORIAL-BACKGROUND

• http://www.cs.utexas.edu/users/moore/publications/km97a.pdf
• https://arxiv.org/abs/1705.01228v1

External links from JAVA____ATJ-TUTORIAL-MOTIVATION

• http://isabelle.in.tum.de
• http://pvs.csl.sri.com
• http://sml-family.org
• http://www.scheme-reports.org
• https://abcl.org
• https://common-lisp.net/project/cffi
• https://coq.inria.fr
• https://docs.oracle.com/javase/10/docs/specs/jni
• https://en.wikipedia.org/wiki/C_%28programming_language%29
• https://hol-theorem-prover.org
• https://ocaml.org
• https://scala-lang.org
• https://www.haskell.org

External links from JAVA____ATJ-TUTORIAL

• https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL22018.1

External links from JAVA____AIJ

• https://www.jetbrains.com/idea

External links from JAVA____GRAMMAR

• https://www.rfc-editor.org/info/rfc5234
• https://www.rfc-editor.org/info/rfc7405

External links from ISAR____ISAR

• https://isabelle.in.tum.de

External links from HTCLIENT____HTCLIENT

• https://github.com/fukamachi/dexador/

External links from ETHEREUM____ETHEREUM

• http://eips.ethereum.org/EIPS/eip-155
• https://ethereum.org
• https://github.com/ethereum/wiki/wiki
• https://github.com/ethereum/yellowpaper

External links from ZKSEMAPHORE____SEMAPHORE

• https://github.com/appliedzkp/semaphore
• https://github.com/appliedzkp/semaphore/blob/master/spec/Semaphore%20Spec.pdf

External links from ZKSEMAPHORE____PEDERSEN-HASH

• https://github.com/appliedzkp/semaphore/blob/master/spec/Semaphore%20Spec.pdf
• https://iden3-docs.readthedocs.io/en/latest/_downloads/4b929e0f96aef77b75bb5cfc0f832151/Pedersen-Hash.pdf

External links from ZKSEMAPHORE____BABY-JUBJUB-ORDER_F28

• https://tools.ietf.org/html/rfc8032

External links from ZKSEMAPHORE____BABY-JUBJUB-ORDER

• https://sagecell.sagemath.org

External links from ZKSEMAPHORE____BABY-JUBJUB

• https://github.com/barryWhiteHat/baby_jubjub

External links from ETHEREUM____MMP-TREES

• https://github.com/ethereum/wiki/wiki/Patricia-Tree

External links from ETHEREUM____HEX-PREFIX

• https://github.com/ethereum/wiki/wiki/Patricia-Tree#specification-compact-encoding-of-hex-sequence-with-optional-terminator

External links from ETHEREUM____RLP

• https://github.com/ethereum/wiki/wiki/RLP

External links from HDWALLET____CRYPTO-HDWALLET

• https://github.com/acl2/acl2/tree/master/books/kestrel/hdwallet/README.md
• https://github.com/satoshilabs/slips/blob/master/slip-0044.md

External links from ETHEREUM____MAKE-SIGNED-TRANSACTION

• https://github.com/ethereum/EIPs/blob/master/EIPS/eip-155.md

External links from R1CS____R1CS

• https://medium.com/@VitalikButerin/quadratic-arithmetic-programs-from-zero-to-hero-f6d558cea649

External links from R1CS____R1CS-VERIFICATION-WITH-AXE

• https://github.com/acl2/acl2/tree/master/books/kestrel/ethereum/semaphore/uint32xor-proof.lisp

External links from KDF____KDF

• https://tools.ietf.org/html/rfc8018

External links from SHA2____SHA-2

• https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf

External links from PADDING____PADDING

• https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf

External links from MIMC____MIMC

• https://docs.zkproof.org/pages/standards/accepted-workshop3/proposal-semaphore.pdf
• https://eprint.iacr.org/2016/492

External links from ZKSEMAPHORE____BABY-JUBJUB-PRIME

• https://en.wikipedia.org/wiki/Quadratic_residue

External links from HMAC____HMAC

• https://tools.ietf.org/html/rfc2104

External links from KECCAK____KECCAK

• https://ethereum.stackexchange.com/questions/550/which-cryptographic-hash-function-does-ethereum-use
• https://keccak.team/files/Keccak-submission-3.pdf

External links from CRYPTO____AES-256-CBC-PKCS7-INTERFACE

• https://csrc.nist.gov/publications/detail/fips/197/final
• https://csrc.nist.gov/publications/detail/sp/800-38a/final
• https://tools.ietf.org/html/rfc2315

External links from CRYPTO____AES-192-CBC-PKCS7-INTERFACE

• https://csrc.nist.gov/publications/detail/fips/197/final
• https://csrc.nist.gov/publications/detail/sp/800-38a/final
• https://tools.ietf.org/html/rfc2315

External links from CRYPTO____AES-128-CBC-PKCS7-INTERFACE

• https://csrc.nist.gov/publications/detail/fips/197/final
• https://csrc.nist.gov/publications/detail/sp/800-38a/final
• https://tools.ietf.org/html/rfc2315

External links from CRYPTO____AES-256-INTERFACE

• https://csrc.nist.gov/publications/detail/fips/197/final

External links from CRYPTO____AES-192-INTERFACE

• https://csrc.nist.gov/publications/detail/fips/197/final

External links from CRYPTO____AES-128-INTERFACE

• https://csrc.nist.gov/publications/detail/fips/197/final

External links from CRYPTO____KECCAK-512-INTERFACE

• https://keccak.team/keccak.html

External links from CRYPTO____KECCAK-256-INTERFACE

• https://keccak.team/keccak.html

External links from ECDSA____DETERMINISTIC-ECDSA-SECP256K1

• http://www.secg.org/sec1-v2.pdf
• https://tools.ietf.org/html/rfc6979

External links from ECDSA____SECP256K1-SIGN-DET-REC

• http://www.secg.org/sec1-v2.pdf
• https://tools.ietf.org/html/rfc6979

External links from ECDSA____SECP256K1-ECDSA-INTERFACE

• http://www.secg.org/sec1-v2.pdf
• http://www.secg.org/sec2-v2.pdf

External links from ECURVE____PRIME-FIELD-SQUARES-EULER-CRITERION

• https://en.wikipedia.org/wiki/Euler's_criterion

External links from ECURVE____SECP256K1

• http://www.secg.org/sec2-v2.pdf#page=13

External links from ECURVE____BIRATIONAL-MONTGOMERY-TWISTED-EDWARDS

• https://eprint.iacr.org/2008/013.pdf
• https://math.stackexchange.com/questions/1391732/birational-equvalence-of-twisted-edwards-and-montgomery-curves

External links from ECURVE____MONTGOMERY-DISTINCT-X-WHEN-NONZERO-MUL-IN-ORDER-RANGE

• https://zips.z.cash/protocol/protocol.pdf

External links from ECURVE____MONTGOMERY

• https://eprint.iacr.org/2008/013.pdf
• https://www.ams.org/journals/mcom/1987-48-177/S0025-5718-1987-0866113-7/

External links from ECURVE____TWISTED-EDWARDS-COMPRESS

• https://zips.z.cash/protocol/protocol.pdf

External links from ECURVE____TWISTED-EDWARDS

• https://eprint.iacr.org/2008/013.pdf

External links from ECURVE____SHORT-WEIERSTRASS-CURVES

• http://www.secg.org/sec1-v2.pdf

External links from C____C

• https://gcc.gnu.org/onlinedocs/gcc/
• https://gcc.gnu.org/onlinedocs/gcc/C-Extensions.html
• https://www.iso.org/standard/74528.html
• https://www.iso.org/standard/82075.html

External links from C_42____VALID-STMT

• GCC statement expressions

External links from C_42____READ-CHAR

• https://en.wikipedia.org/wiki/Trojan_Source
• https://en.wikipedia.org/wiki/UTF-8

External links from C_42____ATTRIB-SPEC

• https://gcc.gnu.org/onlinedocs/gcc/Attribute-Syntax.html

External links from C_42____ATTRIB

• https://gcc.gnu.org/onlinedocs/gcc/Attribute-Syntax.html

External links from C_42____TYPE-SPEC

• https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
• https://gcc.gnu.org/onlinedocs/gcc/_005f_005fint128.html

External links from C_42____ASM-NAME-SPEC

• https://gcc.gnu.org/onlinedocs/gcc/Asm-Labels.html

External links from C_42____ABSTRACT-SYNTAX

• https://eli.thegreenplace.net/2007/11/24/the-context-sensitivity-of-cs-grammar/
• https://en.wikipedia.org/wiki/Lexer_hack
• https://stackoverflow.com/questions/17202409/how-typedef-name-identifier-issue-is-resolved-in-c
• https://web.archive.org/web/20131109145649/https://eli.thegreenplace.net/2011/05/02/the-context-sensitivity-of-cs-grammar-revisited/
• https://www.gnu.org/software/bison/manual/bison.html#Context-Dependency

External links from BITCOIN____BITCOIN

• https://bitcoin.org
• https://bitcoin.org/bitcoin.pdf
• https://en.bitcoin.it
• https://github.com/bitcoin/bips
• https://github.com/bitcoinbook/bitcoinbook

External links from BITCOIN____BECH32

• https://github.com/bitcoin/bips/blob/master/bip-0173.mediawiki
• https://github.com/bitcoin/bips/blob/master/bip-0350.mediawiki

External links from BITCOIN____BIP44

• https://en.bitcoin.it/wiki/BIP_0044
• https://github.com/bitcoin/bips/blob/master/bip-0044.mediawiki

External links from BITCOIN____BIP43

• https://en.bitcoin.it/wiki/BIP_0043
• https://github.com/bitcoin/bips/blob/master/bip-0043.mediawiki

External links from BITCOIN____BIP39

• https://en.bitcoin.it/wiki/BIP_0039
• https://github.com/bitcoin/bips/blob/master/bip-0039.mediawiki
• https://github.com/ethereumbook/ethereumbook/blob/develop/05wallets.asciidoc

External links from BITCOIN_____A2BIP39-ENGLISH-WORDS_A2

• https://github.com/bitcoin/bips/blob/master/bip-0039/english.txt

External links from CRYPTO____PBKDF2-HMAC-SHA-512-INTERFACE

• https://tools.ietf.org/html/rfc8018

External links from CRYPTO____DEFINTERFACE-PBKDF2

• https://tools.ietf.org/html/rfc8018

External links from BITCOIN____BIP32

• https://en.bitcoin.it/wiki/BIP_0032
• https://github.com/bitcoin/bips/blob/master/bip-0032.mediawiki

External links from ECURVE____SECP256K1-INTERFACE

• http://www.secg.org/sec1-v2.pdf
• http://www.secg.org/sec2-v2.pdf

External links from ECURVE____SECP256K1-TYPES

• http://www.secg.org/sec1-v2.pdf
• http://www.secg.org/sec2-v2.pdf

External links from ECURVE____SECP256K1-DOMAIN-PARAMETERS

• http://www.secg.org/sec1-v2.pdf
• http://www.secg.org/sec2-v2.pdf

External links from CRYPTO____HMAC-SHA-512-INTERFACE

• https://tools.ietf.org/html/rfc2104

External links from CRYPTO____SHA-512-INTERFACE

• https://csrc.nist.gov/publications/detail/fips/180/4/final

External links from CRYPTO____DEFINTERFACE-HMAC

• https://tools.ietf.org/html/rfc2104

External links from BITCOIN____BASE58CHECK-ENCODE

• https://en.bitcoin.it/wiki/Base58Check_encoding#Creating_a_Base58Check_string
• https://en.bitcoin.it/wiki/List_of_address_prefixes

External links from BITCOIN____BASE58CHECK

• https://en.bitcoin.it/wiki/Base58Check_encoding

External links from BITCOIN____BASE58-ENCODE

• https://en.bitcoin.it/wiki/Base58Check_encoding#Creating_a_Base58Check_string

External links from BITCOIN_____A2BASE58-CHARACTERS_A2

• https://en.bitcoin.it/wiki/Base58Check_encoding#Base58_symbol_chart

External links from BITCOIN____BASE58

• https://en.bitcoin.it/wiki/Base58Check_encoding

External links from CRYPTO____SHA-256-INTERFACE

• https://csrc.nist.gov/publications/detail/fips/180/4/final

External links from CRYPTO____RIPEMD-160-INTERFACE

• https://homes.esat.kuleuven.be/~bosselae/ripemd160/pdf/AB-9601/AB-9601.pdf

External links from ACL2____AXE

• https://www.kestrel.edu/research/axe/

External links from ACL2____STP

• https://github.com/stp/stp

External links from APT____APT

• http://www.kestrel.edu/home/projects/apt
• images/res/kestrel-apt-images/apt-logo.png

External links from APT____TAILREC

• res/kestrel-apt-design-notes/tailrec.pdf
• res/kestrel-design-notes/notation.pdf

External links from APT____SOLVE

• http://eptcs.web.cse.unsw.edu.au/paper.cgi?ACL22015.3
• https://www.isa-afp.org/entries/Pop_Refinement.html
• res/kestrel-apt-design-notes/solve.pdf
• res/kestrel-design-notes/notation.pdf

External links from APT____SCHEMALG-DIVCONQ-OSET-0-1

• res/kestrel-apt-design-notes/schemalg.pdf

External links from APT____SCHEMALG-DIVCONQ-LIST-0-1

• res/kestrel-apt-design-notes/schemalg.pdf

External links from APT____SCHEMALG

• http://eptcs.web.cse.unsw.edu.au/paper.cgi?ACL22015.3
• res/kestrel-apt-design-notes/schemalg.pdf
• res/kestrel-apt-design-notes/specs-refs.pdf
• res/kestrel-design-notes/notation.pdf

External links from APT____RESTRICT

• res/kestrel-apt-design-notes/restrict.pdf
• res/kestrel-design-notes/notation.pdf

External links from APT____PARTEVAL

• res/kestrel-apt-design-notes/parteval.pdf
• res/kestrel-design-notes/notation.pdf

External links from APT____ISODATA

• res/kestrel-apt-design-notes/isodata.pdf
• res/kestrel-design-notes/notation.pdf

External links from APT____EXPDATA

• res/kestrel-apt-design-notes/expdata.pdf
• res/kestrel-apt-design-notes/isodata.pdf
• res/kestrel-design-notes/notation.pdf

External links from APT____CASESPLIT

• res/kestrel-apt-design-notes/casesplit.pdf
• res/kestrel-design-notes/notation.pdf

External links from APT____SPECIFICATION-FORMS

• res/kestrel-apt-design-notes/specs-refs.pdf
• res/kestrel-design-notes/notation.pdf

External links from ACL2PL____ACL2-PROGRAMMING-LANGUAGE

• http://www.cs.utexas.edu/users/moore/publications/km97a.pdf

External links from ACL2PL____STEP-FROM-TRANS

• https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node61.html#SECTION00915000000000000000

External links from ACL2____EQUATIONAL

• http://www.mcs.anl.gov/research/projects/AR/

External links from ACL2____WP-GEN

• mailto:seweissman@gmail.com

External links from ACL2____SHA-2

• http://en.wikipedia.org/wiki/SHA-2

External links from ACL2____DES

• http://en.wikipedia.org/wiki/Data_Encryption_Standard

External links from ACL2____JFKR

• http://dx.doi.org/10.1145/1637837.1637854

External links from ACL2____TASPI

• http://dx.doi.org/10.1007/11557067_29
• http://www.ccs.neu.edu/home/pete/acl206/papers/hunt.pdf
• https://repositories.lib.utexas.edu/bitstream/handle/2152/ETD-UT-2009-12-529/NELESEN-DISSERTATION.pdf

External links from ACL2____ZFC-MODEL

• https://en.wikipedia.org/wiki/Axiom_of_global_choice
• https://en.wikipedia.org/wiki/Von_Neumann_universe
• https://en.wikipedia.org/wiki/Zermelo-Fraenkel_set_theory

External links from ACL2____ZFC

• https://isabelle.in.tum.de/dist/Isabelle2024/doc/logics-ZF.pdf

External links from ECURVE____BLS12-377-DOMAIN-PARAMETERS

• https://eprint.iacr.org/2018/962.pdf

External links from ABNF____ABNF

• https://www.kestrel.edu/home/people/coglio/vstte18.pdf
• https://www.rfc-editor.org/info/rfc3501
• https://www.rfc-editor.org/info/rfc3986
• https://www.rfc-editor.org/info/rfc5234
• https://www.rfc-editor.org/info/rfc5321
• https://www.rfc-editor.org/info/rfc5322
• https://www.rfc-editor.org/info/rfc7159
• https://www.rfc-editor.org/info/rfc7230
• https://www.rfc-editor.org/info/rfc7405

External links from ABNF____PDF-EXAMPLE

• https://www.iso.org/standard/75839.html

External links from ABNF____IMAP-EXAMPLE

• https://www.rfc-editor.org/info/rfc3501

External links from ABNF____SMTP-EXAMPLE

• https://www.rfc-editor.org/info/rfc5321

External links from ABNF____IMF-EXAMPLE

• https://www.rfc-editor.org/info/rfc5322

External links from ABNF____HTTP-EXAMPLE

• https://www.rfc-editor.org/info/rfc7230

External links from ABNF____URI-EXAMPLE

• https://www.rfc-editor.org/info/rfc3986

External links from ABNF____REMOVAL

• https://www.rfc-editor.org/info/rfc5321
• https://www.rfc-editor.org/info/rfc5322

External links from ABNF____RENAMING

• https://www.rfc-editor.org/info/rfc3986
• https://www.rfc-editor.org/info/rfc7230

External links from ABNF____PLUGGING

• https://www.rfc-editor.org/info/rfc3986
• https://www.rfc-editor.org/info/rfc7230

External links from ALEO____ALEO

• https://provable.com
• https://www.aleo.org

External links from LEO____LEO

• https://aleo.org
• https://provable.com
• https://www.leo-lang.org

External links from ALEOBFT____ALEOBFT

• https://aleo.org
• https://arxiv.org/abs/2105.11827
• https://arxiv.org/abs/2201.05677
• https://arxiv.org/abs/2209.05633
• https://github.com/AleoNet/snarkOS
• https://github.com/AleoNet/snarkVM

External links from POSEIDON____POSEIDON

• https://eprint.iacr.org/2019/1107
• https://www.poseidon-hash.info

External links from POSEIDON____POSEIDON-INGONYAMA-BLS-255-NEPTUNE

• https://github.com/ingonyama-zk/poseidon-hash

External links from POSEIDON____POSEIDON-INGONYAMA-BLS-255

• https://github.com/ingonyama-zk/poseidon-hash

External links from POSEIDON____POSEIDON-INGONYAMA-BN-254

• https://github.com/ingonyama-zk/poseidon-hash

External links from POSEIDON____POSEIDON-RATE-8-ALPHA-17

• https://developer.aleo.org/aleo/opcodes#hashpsd8

External links from POSEIDON____POSEIDON-RATE-4-ALPHA-17

• https://developer.aleo.org/aleo/opcodes#hashpsd4

External links from POSEIDON____POSEIDON-RATE-2-ALPHA-17

• https://developer.aleo.org/aleo/opcodes#hashpsd2

External links from SMT____Z3-INSTALLATION

• https://github.com/Z3Prover/z3/releases

External links from SMT____SMTLINK

• http://smtlib.cs.uiowa.edu/
• https://arxiv.org/abs/1509.06082
• https://github.com/Z3Prover/z3/
• https://github.com/Z3Prover/z3/wiki

External links from ACL2____VWSIM-TUTORIAL-3

• images/res/vwsim-images/d-latch-top-level.png
• images/res/vwsim-images/d-latch.png

External links from ACL2____VWSIM-TUTORIAL-2

• images/res/vwsim-images/jtl4-top-level.png
• images/res/vwsim-images/jtl4.png

External links from ACL2____VW-PLOT-COMMAND

• http://www.gnuplot.info

External links from ACL2____VWSIM-BUILD-AND-SETUP

• https://www.cs.utexas.edu/users/moore/acl2/current/HTML/installation/installation.html

External links from ACL2____VWSIM

• images/res/vwsim-images/VWSIM-Flowchart-Small.png

External links from RP____MULTIPLIER-VERIFICATION-DEMO-3

• https://github.com/acl2/acl2/blob/master/books/projects/vescmul/demo/homma-7-to-3-64x64-signed-carry-select.v

External links from RP____MULTIPLIER-VERIFICATION-DEMO-2-EXPANDED

• https://github.com/acl2/acl2/blob/master/books/projects/vescmul/demo/integrated_multipliers.sv

External links from RP____MULTIPLIER-VERIFICATION-DEMO-2

• https://github.com/acl2/acl2/blob/master/books/projects/vescmul/demo/integrated_multipliers.sv
• https://temelmertcan.github.io/vescmul.zip

External links from RP____MULTIPLIER-VERIFICATION-DEMO-1

• https://temelmertcan.github.io/vescmul.zip

External links from ACL2____VESCMUL

• http://doi.org/10.1007/978-3-030-53288-8_23
• http://doi.org/10.34727/2021/isbn.978-3-85448-046-4_13
• https://repositories.lib.utexas.edu/handle/2152/88056
• https://temelmertcan.github.io/vescmul.zip

External links from ACL2____RP-REWRITER

• https://doi.org/10.48550/arXiv.2009.13765
• https://doi.org/10.48550/arXiv.2205.11703

External links from IRV____FAIRNESS-CRITERIA

• https://en.m.wikipedia.org/wiki/Instant-runoff_voting#Satisfied_Criteria

External links from DIMACS-READER____DIMACS-READER

• http://dimacs.rutgers.edu/Challenges/
• http://www-cs-faculty.stanford.edu/~uno/taocp.html
• http://www.satcompetition.org/2009/format-benchmarks2009.html

External links from PROOF-CHECKER-ARRAY____PROOF-CHECKER-ARRAY

• http://www.cs.utexas.edu/~nwetzler/publications/dissertation-preprint.pdf
• https://repositories.lib.utexas.edu/handle/2152/30538

External links from PROOF-CHECKER-ITP13____PROOF-CHECKER-ITP13

• http://link.springer.com/chapter/10.1007%2F978-3-642-39634-2_18
• http://www.cs.utexas.edu/~nwetzler/publications/itp13.pdf

External links from FARRAY____FARRAY

• http://www.cs.utexas.edu/users/moore/acl2/seminar/2015.01.27-wetzler/farray-diagram.pdf
• http://www.cs.utexas.edu/users/moore/acl2/seminar/2015.01.27-wetzler/farray-talk-20150127.lisp
• http://www.cs.utexas.edu/~nwetzler/publications/dissertation-preprint.pdf
• https://repositories.lib.utexas.edu/handle/2152/30538

External links from ACL2____X86ISA

• images/res/x86isa/x86isa.png

External links from X86ISA____MODEL-VALIDATION

• images/res/x86isa/cosim.png

External links from X86ISA____X86ISA-BUILD-INSTRUCTIONS

• http://ccl.clozure.com/

External links from X86ISA____INTRODUCTION

• http://www.intel.com/content/www/us/en/processors/architectures-software-developer-manuals.html
• https://developer.amd.com/resources/developer-guides-manuals/

External links from X86ISA____BUILDING-ROOTFS

• https://dl-cdn.alpinelinux.org/alpine/v3.21/releases/x86_64/

External links from X86ISA____RUNNING-LINUX

• http://www.cs.utexas.edu/users/hunt/x86-ISA/linux

External links from X86ISA____PROGRAM-EXECUTION

• http://en.wikipedia.org/wiki/Executable_and_Linkable_Format
• http://en.wikipedia.org/wiki/Mach-O
• http://www.agner.org/optimize/calling_conventions.pdf
• http://www.x86-64.org/documentation/abi.pdf

External links from X86ISA____X86-RDRAND

• http://software.intel.com/en-us/articles/intel-digital-random-number-generator-drng-software-implementation-guide/

External links from X86ISA____SELECT-OPERAND-SIZE

• images/res/x86isa/Vol-1-Table-3-3-small.png
• images/res/x86isa/Vol-1-Table-3-4-small.png

External links from X86ISA____EA-TO-LA

• https://www.embedded.com/electronics-blogs/significant-bits/4024943/Taming-the-x86-beast

External links from ACL2____SIDEKICK

• http://ccl.clozure.com
• res/sidekick/eclipse.png
• res/sidekick/emacs.png

External links from ACL2____REGEX

• http://www.gnu.org/software/grep/manual/grep.html#Regular-Expressions

External links from MILAWA____FINAL-CHECKS

• http://clisp.cons.org/
• http://sbcl.sourceforge.net/
• http://trac.clozure.com/openmcl
• http://www.allegrocache.org/support/tech_corner/lisp-heap-051508.lhtml
• http://www.cons.org/cmucl/
• http://www.franz.com/products/allegrocl/
• http://www.scieneer.com/scl/

External links from MILAWA____BUILD

• https://github.com/acl2/acl2

External links from MILAWA____JITAWA

• http://www.cl.cam.ac.uk/~mom22/jitawa/
• https://www.kookamara.com/jared/milawa/Documentation/Talks/2012-northeastern/milawa-northeastern.pdf
• https://www.kookamara.com/jared/publications/2011-itp-jitawa/2011-itp-jitawa.pdf
• https://www.kookamara.com/jared/publications/2012-itp-milawa/2012-itp-milawa.pdf

External links from ACL2____MILAWA

• ftp://ftp.cs.utexas.edu/pub/techreports/tr08-14.pdf
• http://hol.sourceforge.net/
• http://www.cl.cam.ac.uk/~mom22/index.html
• http://www.cl.cam.ac.uk/~mom22/jitawa/
• http://www.cs.uwyo.edu/~ruben/acl2-07/
• http://www.darpa.mil/
• http://www.gnu.org/philosophy/free-sw.html
• http://www.nsf.gov/
• https://www.kookamara.com/jared/
• https://www.kookamara.com/jared/milawa/Documentation/Proposal/oral/proposal.pdf
• https://www.kookamara.com/jared/milawa/Documentation/Proposal/proposal-web.pdf
• https://www.kookamara.com/jared/milawa/Documentation/Rewriter/rewrite.pdf
• https://www.kookamara.com/jared/milawa/Documentation/Talks/2005-11-acl2-talk/talk.pdf
• https://www.kookamara.com/jared/milawa/Documentation/Talks/2006-summer-acl2/talk.pdf
• https://www.kookamara.com/jared/milawa/Documentation/Talks/2007-03-28-acl2-meeting/Update.pdf
• https://www.kookamara.com/jared/milawa/Documentation/Talks/2007-11-acl2-rewriter/rewriter.pdf
• https://www.kookamara.com/jared/milawa/Documentation/defense.pdf
• https://www.kookamara.com/jared/milawa/Documentation/dissertation.pdf

External links from VL2014____VL-MATCH-LATCH-MAIN

• http://www.sunburst-design.com/papers/

External links from VL2014____EDGESYNTH

• images/res/vl/always/edgesynth_reset.png

External links from VL2014____LINT

• http://en.wikipedia.org/wiki/Lint_%28software%29

External links from VL2014____EXPRESSION-SIZING-MINUTIA

• http://www.boydtechinc.com/btf/archive/btf_1999/0642.html
• http://www.eda.org/svdb/bug_view_page.php?bug_id=0001072

External links from VL2014____JSON-PRINTING

• http://www.json.org/

External links from VL2014____URL-ENCODING

• http://tools.ietf.org/html/rfc3986

External links from VL2014____WARNINGS

• https://en.wikipedia.org/wiki/Assertion_(software_development)
• https://en.wikipedia.org/wiki/Exception_handling

External links from VL2014____SUPPORTED-CONSTRUCTS

• http://standards.ieee.org/findstds/standard/1364-2005.html
• http://standards.ieee.org/findstds/standard/1800-2012.html

External links from VL2014____GETTING-STARTED

• http://en.wikipedia.org/wiki/SystemVerilog
• http://en.wikipedia.org/wiki/Verilog
• http://www.cs.bham.ac.uk/research/projects/formare/events/aisb2013/
• https://www.kookamara.com/jared/2013-doform-embedding.pdf

External links from ACL2____VL2014

• http://en.wikipedia.org/wiki/SystemVerilog
• http://en.wikipedia.org/wiki/Verilog

External links from SV____SV-VERSUS-ESIM

• http://www.oracle.com

External links from VL____WARNING-BASICS

• https://en.wikipedia.org/wiki/Assertion_(software_development)
• https://en.wikipedia.org/wiki/Exception_handling

External links from VL____SUPPORTED-CONSTRUCTS

• http://standards.ieee.org/findstds/standard/1364-2005.html
• http://standards.ieee.org/findstds/standard/1800-2012.html

External links from VL____GETTING-STARTED

• http://en.wikipedia.org/wiki/SystemVerilog
• http://en.wikipedia.org/wiki/Verilog
• http://www.cs.bham.ac.uk/research/projects/formare/events/aisb2013/
• https://www.kookamara.com/jared/2013-doform-embedding.pdf

External links from ACL2____VL

• http://en.wikipedia.org/wiki/SystemVerilog
• http://en.wikipedia.org/wiki/Verilog

External links from VL____VL-LINT

• http://en.wikipedia.org/wiki/Lint_%28software%29

External links from VL____JSON-PRINTING

• http://www.json.org/

External links from VL____PRINTER

• https://www.ietf.org/rfc/rfc3986.txt

External links from GL____5._02Using_02def-gl-thm

• http://dx.doi.org/10.1145/309847.309968

External links from GL____3._02Computing_02with_02Symbolic_02Objects

• http://www-formal.stanford.edu/jmc/recursive.pdf

External links from GL____1._02An_02Example_02GL_02Proof

• http://graphics.stanford.edu/~seander/bithacks.html

External links from GL____CASE-SPLITTING

• http://dx.doi.org/10.1007/BFb0028769
• http://dx.doi.org/10.1145/309847.309968

External links from GL____OTHER-RESOURCES

• http://dl.acm.org/citation.cfm?id=1841184
• http://dx.doi.org/10.1007/978-3-642-14052-5_30
• http://dx.doi.org/10.1109/MEMCOD.2011.5970515
• http://dx.doi.org/10.1145/1637837.1637840
• http://dx.doi.org/10.4204/EPTCS.114.8
• http://dx.doi.org/10.4204/EPTCS.70.7
• http://repositories.lib.utexas.edu/handle/2152/ETD-UT-2010-12-2210

External links from ACL2____GL

• http://en.wikipedia.org/wiki/Binary_decision_diagram
• http://en.wikipedia.org/wiki/Boolean_satisfiability_problem

External links from AIGNET____AIGNET-READ-AIGER

• http://fmv.jku.at/aiger/

External links from AIGNET____AIGNET-WRITE-AIGER

• http://fmv.jku.at/aiger/

External links from AIGNET____AIGNET-CONSTRUCTION

• http://megaknowledge.info/cadathlon/2007/refs/p5-verification.pdf

External links from AIGNET____MAYBE-LITP

• https://en.wikipedia.org/wiki/Option_type

External links from ACL2____AIGNET

• http://dx.doi.org/10.4204/EPTCS.114.8
• http://www.eecs.berkeley.edu/~alanmi/abc/
• images/res/aignet/combinational.png

External links from ACL2____DEFSTRUCTURE

• http://www.cs.utexas.edu/users/moore/acl2

External links from IPASIR____IPASIR

• https://github.com/biotomas/ipasir

External links from IPASIR____BUILDING-AN-IPASIR-SOLVER-LIBRARY

• https://github.com/audemard/glucose
• https://github.com/biotomas/ipasir
• https://github.com/liveontologies/ipasir
• https://satcompetition.github.io/2020/downloads.html

External links from ACL2S-INTERFACE____ACL2S-INTERFACE-SYMBOL-PACKAGE-TIPS

• http://www.sbcl.org/manual/#Extended-Package-Prefix-Syntax

External links from ACL2S____ACL2S-IMPLEMENTATION-NOTES

• bobs_mode.jar

External links from ACL2S____ACL2S-USER-GUIDE

• http://arxiv.org/pdf/1105.4394v2.pdf
• images/res/acl2s/icons/acl2_book.gif
• images/res/acl2s/icons/acl2_clean.gif
• images/res/acl2s/icons/acl2_interrupt.gif
• images/res/acl2s/icons/acl2_restart.gif
• images/res/acl2s/icons/acl2_stop.gif
• images/res/acl2s/icons/advance.gif
• images/res/acl2s/icons/cancel.gif
• images/res/acl2s/icons/clean.gif
• images/res/acl2s/icons/move.gif
• images/res/acl2s/icons/retreat.gif
• images/res/acl2s/mac-command.gif
• res/acl2s/sheet.pdf

External links from ACL2S____ACL2S-FAQ

• http://help.eclipse.org/2022-06/topic/org.eclipse.platform.doc.user/gettingStarted/qs-02a.htm
• http://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html
• http://www.cs.utexas.edu/~moore/acl2/
• http://www.eclipse.org
• http://www.eclipse.org/documentation/main.html

External links from ACL2S____ACL2S-TUTORIAL

• http://help.eclipse.org/2022-09/topic/org.eclipse.platform.doc.user/gettingStarted/qs-02a.htm
• https://support.apple.com/guide/mac-help/control-access-to-files-and-folders-on-mac-mchld5a35146/mac
• images/res/acl2s/icons/acl2_restart.gif
• images/res/acl2s/icons/advance.gif
• images/res/acl2s/mac-command.gif
• images/res/acl2s/new_persp.gif

External links from ACL2S____ACL2S-UPDATING-MACOS-OR-LINUX

• images/res/acl2s/updating/available-updates.png
• images/res/acl2s/updating/trust.png

External links from ACL2S____ACL2S-INSTALLATION-FAQ

• https://bugs.eclipse.org/bugs/show_bug.cgi?id=494293
• https://www.architectryan.com/2018/03/17/add-to-the-path-on-windows-10/

External links from ACL2S____ACL2S-INSTALLATION-LINUX

• https://brew.sh
• https://www.eclipse.org/downloads/download.php?file=/technology/epp/downloads/release/2024-06/R/eclipse-java-2024-06-R-linux-gtk-x86_64.tar.gz&r=1
• https://youtu.be/FVgDt0gHTTw

External links from ACL2S____ACL2S-INSTALLATION-MACOS

• https://brew.sh
• https://bugs.eclipse.org/bugs/show_bug.cgi?id=494293
• https://www.eclipse.org/downloads/download.php?file=/technology/epp/downloads/release/2024-06/R/eclipse-java-2024-06-R-macosx-cocoa-aarch64.dmg&r=1
• https://www.eclipse.org/downloads/download.php?file=/technology/epp/downloads/release/2024-06/R/eclipse-java-2024-06-R-macosx-cocoa-x86_64.dmg&r=1
• https://www.oracle.com/java/technologies/downloads/#jdk17-mac
• https://youtu.be/X21cDY06X8E

External links from ACL2S____ACL2S-INSTALLATION-WINDOWS

• https://docs.microsoft.com/en-us/windows/wsl/about
• https://github.com/acl2s/homebrew-acl2s/releases/download/acl2s-0.1.14/ACL2sInstallerWin10.exe
• https://github.com/acl2s/homebrew-acl2s/releases/download/acl2s-0.1.14/ACL2sInstallerWin11.exe
• https://github.com/acl2s/homebrew-acl2s/releases/download/acl2s-0.1.14/distro.tar.gz
• https://github.com/acl2s/homebrew-acl2s/releases/download/acl2s-0.1.8/acl2s-vcxsrv.xlaunch
• https://github.com/acl2s/homebrew-acl2s/releases/download/acl2s-0.1.8/run-acl2s-manual.bat
• https://sourceforge.net/projects/vcxsrv/files/vcxsrv/1.20.14.0/vcxsrv.1.20.14.0.installer.exe/download
• https://youtu.be/Pwf2GWGBTD0
• https://youtu.be/aunZ1K5BIrg

External links from ACL2____SET-TERMINATION-METHOD

• CCG-hierarchy

External links from ACL2____CGEN

• http://arxiv.org/abs/1105.4394v2

External links from ACL2____DEFDATA

• http://arxiv.org/abs/1406.1557

External links from ACL2____DEFPUN

• http://www.cs.utexas.edu/users/moore/acl2/workshop-2000/
• http://www.cs.utexas.edu/users/moore/publications/defpun/index.html

External links from ACL2____DEVELOPERS-GUIDE

• http://www.cs.utexas.edu/users/moore/acl2/workshop-devel-2017/
• https://github.com/acl2/acl2/blob/master/books/system/to-do.txt
• https://www.cs.utexas.edu/users/moore/acl2/workshop-2009/final/10/10.pdf
• mailto:kaufmann@cs.utexas.edu

External links from ACL2____DEVELOPERS-GUIDE-EXAMPLES

• https://www.cs.utexas.edu/users/moore/acl2/manuals/movies/2023-03-31-Developer-Talk.mov
• https://www.cs.utexas.edu/users/moore/acl2/workshop-2009/
• https://www.cs.utexas.edu/users/moore/acl2/workshop-2009/final/10/10.pdf
• https://www.cs.utexas.edu/users/moore/acl2/workshop-2009/presentations/kaufmann-evisc.pdf
• https://www.cs.utexas.edu/users/moore/acl2/workshop-devel-2017/
• https://www.cs.utexas.edu/users/moore/acl2/workshop-devel-2018/

External links from ACL2____DEVELOPERS-GUIDE-RELEASES

• https://github.com/acl2/acl2

External links from ACL2____DEVELOPERS-GUIDE-PROGRAMMING

• http://thesaurus.com

External links from ACL2____DEVELOPERS-GUIDE-INTRODUCTION

• https://github.com/acl2/acl2

External links from ACL2____EQUAL-BY-EVAL-BDDS

• http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/
• http://www.cs.utexas.edu/~jared/publications/2004-acl2-osets/set-theory.pdf

External links from ACL2____UBDDS

• http://en.wikipedia.org/wiki/Binary_decision_diagram

External links from STR____PRETTY-PRINTING-IMPLEMENTATION

• http://www.cs.utexas.edu/~boyer/pretty-print.pdf

External links from STR____BASE64

• http://www.ietf.org/rfc/rfc4648.txt

External links from ACL2____LOGICAL-STORY-OF-IO

• http://www.ccs.neu.edu/home/pete/acl206/papers/davisb.pdf

External links from ACL2____OSICAT

• https://osicat.common-lisp.dev/

External links from ACL2____QUICKLISP

• http://common-lisp.net/project/cl-json/
• http://quickdocs.org/
• http://rubygems.org/
• http://weitz.de/cl-fad/
• http://www.cliki.net/
• http://www.cliki.net/Current%20recommended%20libraries
• http://www.cpan.org/
• http://www.perl.org/
• http://www.quicklisp.org
• http://www.quicklisp.org/beta/bundles.html
• http://www.ruby-lang.org/
• https://brew.sh

External links from SATLINK____UNSAT-CHECKING

• http://www.cs.utexas.edu/~marijn/drat-trim/

External links from SATLINK____SAT-SOLVER-OPTIONS

• http://fmv.jku.at/kissat/
• http://fmv.jku.at/lingeling/
• http://tools.computational-logic.org/content/riss3g.php
• http://www.cril.univ-artois.fr/~hoessen/penelope.html
• http://www.labri.fr/perso/lsimon/glucose/
• http://www.satcompetition.org/
• http://www.satcompetition.org/2013/results.shtml
• https://github.com/arminbiere/kissat

External links from ACL2____SATLINK

• http://fmv.jku.at/lingeling/
• http://www.labri.fr/perso/lsimon/glucose/
• http://www.satcompetition.org/
• https://en.wikipedia.org/wiki/Boolean_satisfiability_problem

External links from SATLINK____DIMACS

• http://www.satcompetition.org/2009/format-benchmarks2009.html
• http://www.satcompetition.org/2011/rules.pdf

External links from SATLINK____CNF

• http://en.wikipedia.org/wiki/Conjunctive_normal_form

External links from SATLINK____VARP

• http://blog.ezyang.com/2010/08/type-kata-newtypes/

External links from ACL2____AIG-AND

• http://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf

External links from ACL2____GETOPT

• http://perldoc.perl.org/Getopt/Long.html
• https://rubygems.org/gems/trollop/

External links from ACL2____MISC_F2RECORDS

• http://www.cs.utexas.edu/users/moore/acl2/workshop-2002/
• http://www.cs.utexas.edu/users/moore/acl2/workshop-2002/contrib/kaufmann-sumners/rcd.pdf
• http://www.cs.utexas.edu/users/moore/acl2/workshop-2002/contrib/kaufmann-sumners/rcdsld.pdf
• http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/contrib/greve-wilding_defrecord/defrecord.pdf

External links from ACL2____DEF-TYPED-RECORD

• http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/contrib/greve-wilding_defrecord/defrecord.ps

External links from ACL2____DEFMAPPING

• res/std-util-design-notes/defmapping.pdf
• res/std-util-design-notes/notation.pdf

External links from STD____DEFSUM

• https://en.wikipedia.org/wiki/Tagged_union

External links from ACL2____DEFARBREC

• res/std-util-design-notes/defarbrec.pdf
• res/std-util-design-notes/notation.pdf

External links from ACL2____CLEX

• http://flex.sourceforge.net/

External links from ACL2____NREV

• https://en.wikipedia.org/wiki/Map_(higher-order_function)

External links from BRIDGE____BINDINGS

• http://www.ruby-lang.org/

External links from BRIDGE____SECURITY

• http://en.wikipedia.org/wiki/Unix_domain_socket

External links from STR____URL-ENCODING

• http://tools.ietf.org/html/rfc3986
• https://www.ietf.org/rfc/rfc3986.txt

External links from BITOPS____PARITY32

• http://graphics.stanford.edu/~seander/bithacks.html

External links from BITOPS____PARITY4

• http://graphics.stanford.edu/~seander/bithacks.html

External links from ACL2____FAST-LOGEXT

• http://graphics.stanford.edu/~seander/bithacks.html

External links from ACL2____FAST-LOGREV-U8

• http://graphics.stanford.edu/~seander/bithacks.html#ReverseByteWith32Bits

External links from STD____DEFAGGREGATE

• https://en.wikipedia.org/wiki/Dependent_type

External links from ACL2____LOGOPS-BYTE-FUNCTIONS

• http://en.wikipedia.org/wiki/X3J13

External links from BUILD____CERT_F5PARAM

• https://github.com/stp/stp

External links from BUILD____DISTRIBUTED-BUILDS

• http://en.wikipedia.org/wiki/Portable_Batch_System
• http://thoughts.davisjeff.com/2009/11/29/linux-oom-killer/
• http://www.adaptivecomputing.com/products/open-source/maui/
• http://www.adaptivecomputing.com/support/download-center/torque-download/
• http://www.rocksclusters.org/

External links from BUILD____STATIC-MAKEFILES

• http://www.gnu.org/software/make/manual/make.html#Include

External links from BUILD____PRELIMINARIES

• http://www.cs.utexas.edu/~moore/acl2/
• http://www.gnu.org/software/make/
• http://www.perl.org/
• https://code.google.com/p/acl2-books/

External links from BUILD____CERT-PL-ON-WINDOWS

• http://www.cygwin.com/
• http://www.mingw.org/wiki/MSYS
• https://www.virtualbox.org/
• https://www.vmware.com/products/player/
• https://www.vmware.com/products/workstation/

External links from OSLIB____FILE-TYPES

• http://common-lisp.net/project/osicat/
• http://weitz.de/cl-fad/
• http://www.ai.mit.edu/projects/iiip/doc/CommonLISP/HyperSpec/Body/chap-19.html
• http://www.ai.mit.edu/projects/iiip/doc/CommonLISP/HyperSpec/Body/chap-20.html
• http://www.ai.mit.edu/projects/iiip/doc/CommonLISP/HyperSpec/FrontMatter/Chapter-Index.html
• http://www.dwheeler.com/essays/fixing-unix-linux-filenames.html
• http://www.gigamonkeys.com/book/
• http://www.gigamonkeys.com/book/files-and-file-io.html
• http://www.gigamonkeys.com/book/practical-a-portable-pathname-library.html

External links from ACL2____STD_F2OSETS

• https://www.cs.utexas.edu/users/moore/acl2/workshop-2004/contrib/davis/set-theory.pdf
• https://www.cs.utexas.edu/users/moore/acl2/workshop-2004/contrib/davis/workshop-osets-slides.pdf

External links from ACL2_____C3_C3

• http://www.cs.utexas.edu/users/moore/acl2/workshop-2002/contrib/manolios-kaufmann/total-order.pdf

External links from ACL2____ACL2

• http://www.cs.utexas.edu/users/moore/acl2

External links from ACL2____100-THEOREMS

• https://github.com/acl2/acl2/blob/master/books/arithmetic/binomial.lisp
• https://github.com/acl2/acl2/blob/master/books/nonstd/circles/area-of-a-circle/area-of-a-circle-2.lisp
• https://github.com/acl2/acl2/blob/master/books/nonstd/nsa/continuity.lisp
• https://github.com/acl2/acl2/blob/master/books/nonstd/nsa/derivatives.lisp
• https://github.com/acl2/acl2/blob/master/books/nonstd/nsa/exp.lisp
• https://github.com/acl2/acl2/blob/master/books/nonstd/nsa/sqrt-2.lisp
• https://github.com/acl2/acl2/blob/master/books/nonstd/transcendentals/reals-are-uncountable-1.lisp
• https://github.com/acl2/acl2/blob/master/books/nonstd/workshops/1999/calculus/book/fundamental-theorem-of-calculus.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/groups/abelian.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/groups/quotients.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/groups/sylow.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/linear/reduction.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/ballot.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/birthday.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/derangements.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/div3.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/divisors.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/eisenstein.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/euclid.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/euler.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/girard.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/harmonic.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/konigsberg.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/partitions.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/subseq.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/subsets.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/sum4squares.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/sylvester.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/triangular.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/triples.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/numbers/z2q.lisp
• https://github.com/acl2/acl2/blob/master/books/projects/schroeder-bernstein/schroeder-bernstein.lisp
• https://github.com/acl2/acl2/blob/master/books/workshops/2006/cowles-gamboa-euclid/Euclid/prime-fac.lisp
• https://github.com/acl2/acl2/blob/master/books/workshops/2018/gamboa-cowles/complex-polynomials.lisp
• https://github.com/acl2/acl2/blob/master/books/workshops/2018/gamboa-cowles/de-moivre.lisp
• https://github.com/acl2/acl2/blob/master/books/workshops/2018/kwan-greenstreet/cauchy-schwarz.lisp
• https://github.com/acl2/acl2/blob/master/books/workshops/2020/kwan-peng-greenstreet/abstract-cs.lisp
• https://link.springer.com/article/10.1007/BF00244463
• https://philpapers.org/rec/SHAMMA-3
• https://www.cs.ru.nl/~freek/100/
• https://www.cs.utexas.edu/users/boyer/ftp/nqthm/nqthm-1992/examples/shankar/goedel.events

External links from XDOC____ADD-RESOURCE-DIRECTORY

• images/res/centaur/centaur-logo.png

External links from XDOC____KATEX-INTEGRATION

• formula.html
• https://github.com/Khan/KaTeX
• https://www.khanacademy.org/

External links from XDOC____EMACS-LINKS

• http://www.gnu.org/software/emacs/
• https://en.wikipedia.org/wiki/Data_URI_scheme
• https://en.wikipedia.org/wiki/Internet_media_type
• https://www.gnu.org/software/emacs/manual/html_node/emacs/Tags-Tables.html

External links from XDOC____DEPLOYING-MANUALS

• http://www.perl.org

External links from XDOC____SAVE

• download/

External links from XDOC____MARKUP

• http://en.wikipedia.org/wiki/HTML
• http://en.wikipedia.org/wiki/Xml
• https://www.cs.utexas.edu/
• images/res/centaur/centaur-logo.png

External links from ACL2____XDOC

• http://dx.doi.org/10.4204/EPTCS.152.2

External links from ACL2____NOTE-6-4-BOOKS

• download/
• http://code.google.com/p/acl2-books/source/list
• http://fmv.jku.at/aiger/FORMAT
• https://code.google.com/p/acl2-books/wiki/ReleaseVersionNumbers
• javascript:printer_friendly()
• linkcheck.html

External links from ACL2____NOTE-6-5-BOOKS

• http://code.google.com/p/acl2-books/source/list
• http://jenkins-ci.org/
• http://www.sitemaps.org/
• https://code.google.com/p/acl2-books/issues/detail?id=136
• https://code.google.com/p/acl2-books/wiki/ReleaseVersionNumbers

External links from ACL2____NOTE-7-0-BOOKS

• http://jenkins-ci.org/
• https://github.com/acl2/acl2
• https://github.com/acl2/acl2/commits/master
• https://github.com/acl2/acl2/wiki/Release-version-numbers

External links from ACL2____NOTE-7-1-BOOKS

• http://www.quicklisp.org/beta/bundles.html
• https://github.com/acl2/acl2/commits/master
• https://github.com/acl2/acl2/wiki/Release-version-numbers
• https://github.com/jaredcdavis/shellpool

External links from ACL2____NOTE-7-2-BOOKS

• https://github.com/acl2/acl2/commits/master
• https://www.cs.utexas.edu/users/moore/acl2/workshop-2015/

External links from ACL2____NOTE-8-0-BOOKS

• https://github.com/acl2/acl2/commits/master
• https://www.newton.ac.uk/event/bpr

External links from ACL2____NOTE-8-1-BOOKS

• http://www.cs.utexas.edu/users/moore/best-ideas/pltp/index.html
• https://bitcoin.org
• https://ethereum.org
• https://github.com/acl2/acl2/commits/master

External links from ACL2____NOTE-8-2-BOOKS

• https://github.com/acl2/acl2/commits/master

External links from ACL2____NOTE-8-3-BOOKS

• https://github.com/acl2/acl2/commits/master

External links from ACL2____NOTE-8-4-BOOKS

• https://github.com/acl2/acl2/commits/master
• https://junit.org
• json.org

External links from ACL2____NOTE-8-5-BOOKS

• https://github.com/acl2/acl2/commits/master

External links from ACL2____NOTE-8-6-BOOKS

• https://aleo.org
• https://github.com/acl2/acl2/commits/master

External links from ACL2____NOTE-8-7-BOOKS

• https://github.com/acl2/acl2/commits/master

External links from ACL2____TSHELL-ENSURE

• https://github.com/jaredcdavis/shellpool/blob/master/DOC.md

External links from ACL2____TSHELL-START

• https://github.com/jaredcdavis/shellpool/blob/master/DOC.md

External links from ACL2____TSHELL

• https://github.com/jaredcdavis/shellpool/
• https://github.com/jaredcdavis/shellpool/blob/master/DOC.md

External links from ACL2____MAYBE-STRINGP

• https://en.wikipedia.org/wiki/Option_type

External links from ACL2____MAYBE-POSP

• https://en.wikipedia.org/wiki/Option_type

External links from ACL2____MAYBE-INTEGERP

• https://en.wikipedia.org/wiki/Option_type

External links from ACL2____MAYBE-BITP

• https://en.wikipedia.org/wiki/Option_type

External links from ACL2____MAYBE-NATP

• https://en.wikipedia.org/wiki/Option_type

External links from ACL2____RTL

• https://www.springer.com/us/book/9783319955124

External links from BIB____WILDING93

• https://link.springer.com/content/pdf/10.1007/3-540-56922-7_22

External links from BIB____SH98

• https://link.springer.com/chapter/10.1007/BFb0028740

External links from BIB____SAWADA00

• https://www.cs.utexas.edu/~moore/publications/acl2-papers.html#Books

External links from BIB____RM04

• https://www.ece.ufl.edu/wp-content/uploads/sites/119/publications/fmcad04.pdf

External links from BIB____RHMM07

• https://link.springer.com/article/10.1007/s10817-008-9098-1

External links from BIB____PLOTKIN04B

• https://www.sciencedirect.com/science/article/pii/S1567832604000268

External links from BIB____PLOTKIN04A

• https://homepages.inf.ed.ac.uk/gdp/publications/sos_jlap.pdf

External links from BIB____MP02

• https://www.cs.utexas.edu/~moore/publications/m5/apprentice.pdf

External links from BIB____MOORE99B

• https://www.cs.utexas.edu/~moore/publications/multi-v-uni.pdf

External links from BIB____MOORE99A

• https://www.cs.utexas.edu/~moore/publications/tjvm/main.pdf

External links from BIB____MOORE73

• http://www.era.lib.ed.ac.uk/handle/1842/2245

External links from BIB____MOORE19

• https://doi.org/10.1007/s00165-019-00490-3

External links from BIB____MOORE17

• https://www.cs.utexas.edu/~moore/publications/ainni.pdf

External links from BIB____MOORE15

• https://www.cs.utexas.edu/~moore/publications/stateman.pdf

External links from BIB____MOORE14

• https://www.cs.utexas.edu/~moore/publications/m1-is-turing-equiv.pdf

External links from BIB____MOORE03B

• https://www.cs.utexas.edu/~moore/publications/trecia/long.pdf

External links from BIB____MOORE03A

• https://www.cs.utexas.edu/~moore/publications/marktoberdorf-02/main_final.pdf

External links from BIB____MP67

• http://jmc.stanford.edu/articles/mcpain/mcpain.pdf

External links from BIB____MMRV06

• http://ece.ufl.edu/wp-content/uploads/sites/119/publications/lpar06.pdf

External links from BIB____MCCARTHY62

• http://jmc.stanford.edu/articles/towards/towards.pdf

External links from BIB____MANOLIOS00

• https://dl.acm.org/doi/10.5555/646186.683220

External links from BIB____LIU06

• https://www.cs.utexas.edu/~moore/publications/liu-dissertation.pdf

External links from BIB____KMM00B

• https://www.cs.utexas.edu/~moore/publications/acl2-books/acs/index.html

External links from BIB____KMM00A

• https://www.cs.utexas.edu/~moore/publications/acl2-books/car/index.html

External links from BIB____HKMS17

• https://royalsocietypublishing.org/doi/10.1098/rsta.2015.0399

External links from BIB____HK12

• http://apps.cs.utexas.edu/tech_reports/reports/tr/TR-2075.pdf

External links from BIB____HB92

• https://royalsocietypublishing.org/doi/abs/10.1098/rsta.1992.0024

External links from BIB____GOEL16

• https://repositories.lib.utexas.edu/server/api/core/bitstreams/858b2f9b-5532-4b2a-bed1-fb889a265f6c/content

External links from BIB____GHK17

• https://link.springer.com/chapter/10.1007/978-3-319-48628-4_8

External links from BIB____GHKG14

• http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/18_goel.pdf

External links from BIB____GHK13

• http://eptcs.org/content.cgi?ACL22013

External links from BIB____BY96

• https://dl.acm.org/doi/10.1145/227595.227603

External links from BIB____BM97

• https://drive.google.com/file/d/0B2yFYLn0Spf1TloxMjNxdzBWN1E/

External links from BIB____BM96

• https://www.cs.utexas.edu/~moore/publications/bm96.pdf

External links from BIB____BM80

• https://www.cs.utexas.edu/~moore/publications/BDX930-Report-1978-81.pdf

External links from BIB____BM79

• https://archive.org/details/acl_20240626

External links from BIB____BM73

• https://www.cs.utexas.edu/~moore/best-ideas/pltp/index.html
• https://www.cs.utexas.edu/~moore/publications/bm-ijcai-73.pdf
• https://www.cs.utexas.edu/~moore/publications/bm75.pdf

External links from BIB____BM05

• https://www.cs.utexas.edu/~moore/publications/csort/main.pdf

External links from BIB____BKM96

• http://www.cs.utexas.edu/users/moore/publications/bkm96.pdf
• https://www.cs.utexas.edu/~moore/publications/divide_paper.pdf

External links from BIB____BH99

• https://link.springer.com/chapter/10.1007/978-1-4471-0523-7_5#citeas

External links from BIB____BH97

• https://ieeexplore.ieee.org/document/628846

External links from BIB____BGM90

• http://www.cs.utexas.edu/users/moore/publications/controller.pdf

External links from ACL2____You_02Must_02Think_02about_02the_02Use_02of_02a_02Formula_02as_02a_02Rule

• images/res/tours/walking.gif

External links from ACL2____What_02is_02a_02Mechanical_02Theorem_02Prover_82Q_92_02_82cont_92

• images/res/tours/flying.gif
• images/res/tours/interactive-theorem-prover-a.gif

External links from ACL2____What_02is_02a_02Mechanical_02Theorem_02Prover_82Q_92

• images/res/tours/automatic-theorem-prover.gif
• images/res/tours/flying.gif

External links from ACL2____What_02is_02a_02Mathematical_02Logic_82Q_92

• images/res/tours/flying.gif
• images/res/tours/proof.gif

External links from ACL2____What_02is_02Required_02of_02the_02User_82Q_92

• images/res/tours/flying.gif

External links from ACL2____What_02Is_02ACL2_82Q_92

• images/res/tours/flying.gif

External links from ACL2____WINDOWS-INSTALLATION

• http://www.cs.utexas.edu/users/moore/acl2/v3-6/distrib/windows/
• https://en.wikipedia.org/wiki/Windows_Subsystem_for_Linux

External links from ACL2____WARRANT

• http://www.cs.utexas.edu/users/kaufmann/papers/apply/index.html

External links from ACL2____Using_02the_02Associativity_02of_02App_02to_02Prove_02a_02Trivial_02Consequence

• images/res/tours/walking.gif

External links from ACL2____The_02WARNING_02about_02the_02Trivial_02Consequence

• images/res/tours/twarning.gif

External links from ACL2____The_02Tours

• images/res/tours/flying.gif
• images/res/tours/walking.gif

External links from ACL2____The_02Theorem_02that_02App_02is_02Associative

• images/res/tours/twarning.gif
• images/res/tours/walking.gif

External links from ACL2____The_02Simplification_02of_02the_02Induction_02Conclusion_02_82Step_029_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Simplification_02of_02the_02Induction_02Conclusion_02_82Step_028_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Simplification_02of_02the_02Induction_02Conclusion_02_82Step_027_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Simplification_02of_02the_02Induction_02Conclusion_02_82Step_026_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Simplification_02of_02the_02Induction_02Conclusion_02_82Step_025_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Simplification_02of_02the_02Induction_02Conclusion_02_82Step_024_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Simplification_02of_02the_02Induction_02Conclusion_02_82Step_023_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Simplification_02of_02the_02Induction_02Conclusion_02_82Step_022_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Simplification_02of_02the_02Induction_02Conclusion_02_82Step_0212_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Simplification_02of_02the_02Induction_02Conclusion_02_82Step_0211_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Simplification_02of_02the_02Induction_02Conclusion_02_82Step_0210_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Simplification_02of_02the_02Induction_02Conclusion_02_82Step_021_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Simplification_02of_02the_02Induction_02Conclusion_02_82Step_020_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Rules_02used_02in_02the_02Associativity_02of_02App_02Proof

• images/res/tours/twarning.gif

External links from ACL2____The_02Proof_02of_02the_02Associativity_02of_02App

• images/res/tours/green-line.gif
• images/res/tours/walking.gif

External links from ACL2____The_02Induction_02Scheme_02Selected_02for_02the_02App_02Example

• images/res/tours/twarning.gif

External links from ACL2____The_02Final_02Simplification_02in_02the_02Base_02Case_02_82Step_023_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Final_02Simplification_02in_02the_02Base_02Case_02_82Step_022_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Final_02Simplification_02in_02the_02Base_02Case_02_82Step_021_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Final_02Simplification_02in_02the_02Base_02Case_02_82Step_020_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Falling_02Body_02Model

• images/res/tours/pisa.gif

External links from ACL2____The_02Expansion_02of_02ENDP_02in_02the_02Induction_02Step_02_82Step_022_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Expansion_02of_02ENDP_02in_02the_02Induction_02Step_02_82Step_021_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Expansion_02of_02ENDP_02in_02the_02Induction_02Step_02_82Step_020_92

• images/res/tours/green-line.gif

External links from ACL2____The_02Event_02Summary

• images/res/tours/twarning.gif

External links from ACL2____The_02End_02of_02the_02Walking_02Tour

• images/res/tours/flying.gif
• images/res/tours/sitting.gif
• images/res/tours/walking.gif

External links from ACL2____The_02End_02of_02the_02Proof_02of_02the_02Associativity_02of_02App

• images/res/tours/green-line.gif
• images/res/tours/walking.gif

External links from ACL2____The_02End_02of_02the_02Flying_02Tour

• images/res/tours/landing.gif
• images/res/tours/walking.gif

External links from ACL2____The_02Associativity_02of_02App

• images/res/tours/green-line.gif
• images/res/tours/walking.gif

External links from ACL2____The_02Admission_02of_02App

• images/res/tours/green-line.gif
• images/res/tours/walking.gif

External links from ACL2____TUTORIAL3-PHONEBOOK-EXAMPLE

• http://www.cs.utexas.edu/users/moore/acl2/

External links from ACL2____TALKS

• http://www.cs.utexas.edu/users/hunt/index.html
• http://www.cs.utexas.edu/users/kaufmann/selected-presentations.html
• http://www.cs.utexas.edu/users/kaufmann/visions-moore-kaufmann.pdf
• http://www.cs.utexas.edu/users/moore/acl2/seminar/
• http://www.cs.utexas.edu/users/moore/acl2/talks/big-proof-talks/
• http://www.cs.utexas.edu/users/moore/acl2/talks/royal-society/talk.pdf
• http://www.cs.utexas.edu/users/moore/acl2/workshops.html
• http://www.cs.utexas.edu/users/moore/publications/talks/marktoberdorf-08/index.html
• https://www.newton.ac.uk/event/bpr

External links from ACL2____Symbolic_02Execution_02of_02Models

• images/res/tours/computing-machine-5xy.gif
• images/res/tours/flying.gif

External links from ACL2____SYS-CALL

• https://ccl.clozure.com/manual/chapter9.2.html

External links from ACL2____START-HERE

• http://new.proofpad.org
• http://www.cs.utexas.edu/users/moore/acl2/
• http://www.cs.utexas.edu/users/moore/acl2/manuals/latest/index.html
• http://www.cs.utexas.edu/users/moore/publications/acl2-books/acs/index.html
• http://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html
• https://github.com/acl2/acl2/tree/master/books
• https://github.com/mister-walter/acl2-docker
• https://hub.docker.com/r/atwalter/acl2
• https://www.cs.utexas.edu/users/moore/acl2/v8-6/combined-manual/index.html?topic=ACL2____The_02Tours
• https://www.cs.utexas.edu/users/moore/acl2/workshops.html
• https://www.cs.utexas.edu/users/moore/publications/acl2-papers.html
• https://www.cs.utexas.edu/users/moore/publications/how-to-prove-thms/intro-to-acl2.pdf
• https://www.cs.utexas.edu/users/moore/publications/how-to-prove-thms/main.pdf

External links from ACL2____SPECIFIC-KINDS-OF-FORMULAS-AS-REWRITE-RULES

• images/res/tours/twarning.gif

External links from ACL2____SOUNDNESS

• http://www.cs.utexas.edu/users/moore/publications/km97a.pdf
• https://www.cs.utexas.edu/users/moore/publications/encap-story.pdf

External links from ACL2____SET-IPRINT

• http://www.cs.utexas.edu/users/moore/acl2/workshop-2009/

External links from ACL2____SBCL-INSTALLATION-BRIEF

• https://www.sbcl.org
• https://www.sbcl.org/platform-table.html

External links from ACL2____SBCL-INSTALLATION

• https://www.sbcl.org

External links from ACL2____Running_02Models

• images/res/tours/computing-machine-5x7.gif
• images/res/tours/flying.gif

External links from ACL2____Rewrite_02Rules_02are_02Generated_02from_02DEFTHM_02Events

• images/res/tours/twarning.gif
• images/res/tours/walking.gif

External links from ACL2____Revisiting_02the_02Admission_02of_02App

• images/res/tours/green-line.gif
• images/res/tours/twarning.gif
• images/res/tours/walking.gif

External links from ACL2____R-AND-I-ANNOTATED-BIBLIOGRAPHY

• http://www.cs.utexas.edu/users/moore/acl2/
• http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/
• http://www.lispworks.com/documentation/HyperSpec/Front/
• https://github.com/acl2/acl2
• https://www.cs.utexas.edu/users/boyer/ftp/nqthm/
• https://www.cs.utexas.edu/users/moore/publications/acl2-books/acs/index.html
• https://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html
• https://www.cs.utexas.edu/users/moore/publications/km97a.pdf

External links from ACL2____RANDOM_42

• http://www.lispworks.com/documentation/HyperSpec/Front

External links from ACL2____QUANTIFIER-TUTORIAL

• http://www.cs.utexas.edu/users/moore/acl2/contrib/quantifier-exercise-1-solution.html

External links from ACL2____Proving_02Theorems_02about_02Models

• images/res/tours/computing-machine-xxy.gif
• images/res/tours/flying.gif

External links from ACL2____PROVISIONAL-CERTIFICATION

• https://github.com/acl2/acl2/issues/255

External links from ACL2____PROOF-OF-WELL-FOUNDEDNESS

• http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/

External links from ACL2____PROOF-BUILDER

• http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html
• http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#slide29

External links from ACL2____PROGRAMMING-KNOWLEDGE-TAKEN-FOR-GRANTED

• http://www.cs.utexas.edu/users/moore/publications/acl2-programming-exercises1.html
• http://www.cs.utexas.edu/users/moore/publications/hyper-card.html
• images/res/tours/twarning.gif

External links from ACL2____PRE-BUILT-BINARY-DISTRIBUTIONS

• http://backports.debian.org
• http://packages.qa.debian.org/a/acl2.html
• http://www.cs.utexas.edu/users/moore/acl2/
• https://formulae.brew.sh/formula/acl2
• https://github.com/mister-walter/acl2-docker/pkgs/container/acl2
• https://github.com/mister-walter/acl2s-docker/pkgs/container/acl2s
• https://hub.docker.com/r/atwalter/acl2/
• https://hub.docker.com/r/atwalter/acl2s/
• https://ports.macports.org/port/acl2/
• https://www.cs.utexas.edu/~moore/acl2/current/HTML/installation/obtaining-and-installing.html#Build-Particular

External links from ACL2____PRACTICE-FORMULATING-STRONG-RULES-6

• images/res/tours/twarning.gif

External links from ACL2____PRACTICE-FORMULATING-STRONG-RULES-3

• images/res/tours/twarning.gif

External links from ACL2____PRACTICE-FORMULATING-STRONG-RULES-2

• images/res/tours/twarning.gif

External links from ACL2____PRACTICE-FORMULATING-STRONG-RULES-1

• images/res/tours/twarning.gif

External links from ACL2____Overview_02of_02the_02Simplification_02of_02the_02Induction_02Step_02to_02T

• images/res/tours/walking.gif

External links from ACL2____Overview_02of_02the_02Simplification_02of_02the_02Base_02Case_02to_02T

• images/res/tours/walking.gif

External links from ACL2____Overview_02of_02the_02Proof_02of_02a_02Trivial_02Consequence

• images/res/tours/green-line.gif
• images/res/tours/walking.gif

External links from ACL2____Other_02Requirements

• images/res/tours/flying.gif

External links from ACL2____ORDINALS

• http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/

External links from ACL2____OPERATIONAL-SEMANTICS-4_F5_F5HOW-TO-FIND-THINGS

• http://www.cs.utexas.edu/users/moore/acl2/
• https://github.com/acl2/acl2
• https://www.cs.utexas.edu/~moore/acl2/current/HTML/installation/installation.html
• https://www.cs.utexas.edu/~moore/publications/acl2-papers.html#Books

External links from ACL2____OPERATIONAL-SEMANTICS-2_F5_F5OTHER-EXAMPLES

• http://www.cs.utexas.edu/users/moore/acl2/

External links from ACL2____O-P

• http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/

External links from ACL2____NOTE-8-6

• https://github.com/Clozure/ccl/issues/446

External links from ACL2____NOTE-8-5

• https://github.com/acl2/acl2/issues/1395

External links from ACL2____NOTE-8-1

• https://serverfault.com/questions/40144/how-can-i-retrieve-the-absolute-filename-in-a-shell-script-on-mac-os-x

External links from ACL2____NOTE-7-4

• https://github.com/acl2/acl2/
• https://github.com/acl2/acl2/commits/master

External links from ACL2____NOTE-7-3

• https://github.com/acl2/acl2/
• https://github.com/acl2/acl2/commits/master

External links from ACL2____NOTE-7-0

• https://github.com/acl2/acl2

External links from ACL2____NOTE-6-0

• http://www.cs.utexas.edu/users/moore/acl2/open-architecture/

External links from ACL2____NOTE-5-0

• http://code.google.com/p/acl2-books/downloads/

External links from ACL2____NOTE-4-3

• http://acl2-books.googlecode.com/

External links from ACL2____NOTE-4-1

• http://code.google.com/p/acl2-books/source/list

External links from ACL2____NOTE-4-0

• http://code.google.com/p/acl2-books/source/list

External links from ACL2____NOTE-3-6-1

• http://code.google.com/p/acl2-books/source/list
• https://code.google.com/p/acl2-books/wiki/ReleaseVersionNumbers

External links from ACL2____NOTE-3-6

• http://code.google.com/p/acl2-books/source/list
• https://code.google.com/p/acl2-books/wiki/ReleaseVersionNumbers

External links from ACL2____NOTE-3-5

• https://code.google.com/p/acl2-books/wiki/ReleaseVersionNumbers

External links from ACL2____NOTE-2-9-3

• http://www.cs.utexas.edu/users/moore/publications/how-to-prove-thms

External links from ACL2____NOTE-2-6-SYSTEM

• http://www.cs.utexas.edu/users/moore/acl2/

External links from ACL2____Models_02of_02Computer_02Hardware_02and_02Software

• images/res/tours/computing-machine.gif
• images/res/tours/flying.gif

External links from ACL2____Models_02in_02Engineering

• images/res/tours/bridge-analysis.gif
• images/res/tours/bridge.gif

External links from ACL2____Modeling_02in_02ACL2

• images/res/tours/computing-machine-a.gif
• images/res/tours/flying.gif

External links from ACL2____MEMOIZE-PARTIAL

• https://en.wikipedia.org/wiki/Collatz_conjecture

External links from ACL2____MANAGING-ACL2-PACKAGES

• http://www.cs.utexas.edu/users/moore/acl2/contrib/managing-acl2-packages.html

External links from ACL2____LOOP_42-PRIMER

• http://www.lispworks.com/documentation/HyperSpec/Body/m_loop.htm#loop

External links from ACL2____LOGIC-KNOWLEDGE-TAKEN-FOR-GRANTED-INDUCTIVE-PROOF

• images/res/tours/twarning.gif

External links from ACL2____IO

• http://www.lispworks.com/documentation/HyperSpec/Body/23_aba.htm

External links from ACL2____INTRODUCTION-TO-THE-THEOREM-PROVER

• http://link.springer.com/content/pdf/bbm%3A978-1-4615-4449-4%2F1.pdf
• http://www.cs.utexas.edu/users/moore/acl2
• http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html#Books
• http://www.lulu.com/content/1746161
• images/res/tours/twarning.gif

External links from ACL2____INTRODUCTION-TO-THE-DATABASE

• images/res/tours/twarning.gif

External links from ACL2____INTRODUCTION-TO-PROGRAMMING-IN-ACL2-FOR-THOSE-WHO-KNOW-LISP

• http://www.cs.utexas.edu/users/moore/acl2/
• http://www.cs.utexas.edu/users/moore/publications/km97a.pdf

External links from ACL2____INTRODUCTION-TO-KEY-CHECKPOINTS

• images/res/tours/twarning.gif

External links from ACL2____INTRODUCTION-TO-HINTS

• images/res/tours/twarning.gif

External links from ACL2____INTRODUCTION-TO-APPLY_42

• http://www.cs.utexas.edu/users/kaufmann/papers/apply/index.html

External links from ACL2____INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS

• images/res/tours/twarning.gif

External links from ACL2____INTERESTING-APPLICATIONS

• http://www.cs.utexas.edu/users/moore/acl2/workshops.html
• http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html

External links from ACL2____INDUCTION-HEURISTICS

• http://www.cs.utexas.edu/users/moore/publications/acl2-induction-heuristics.pdf

External links from ACL2____How_02To_02Find_02Out_02about_02ACL2_02Functions_02_82cont_92

• images/res/tours/twarning.gif
• images/res/tours/walking.gif

External links from ACL2____How_02To_02Find_02Out_02about_02ACL2_02Functions

• images/res/tours/twarning.gif
• images/res/tours/walking.gif

External links from ACL2____How_02Long_02Does_02It_02Take_02to_02Become_02an_02Effective_02User_82Q_92

• images/res/tours/flying.gif

External links from ACL2____Hey_02Wait_12_02_02Is_02ACL2_02Typed_02or_02Untyped_82Q_92

• images/res/tours/twarning.gif

External links from ACL2____Guiding_02the_02ACL2_02Theorem_02Prover

• images/res/tours/interactive-theorem-prover.gif
• images/res/tours/walking.gif

External links from ACL2____Guessing_02the_02Type_02of_02a_02Newly_02Admitted_02Function

• images/res/tours/twarning.gif

External links from ACL2____Guards_02in_02ACL2

• images/res/tours/twarning.gif

External links from ACL2____GUARANTEES-OF-THE-TOP-LEVEL-LOOP

• http://www.cs.utexas.edu/users/kaufmann/papers/apply/index.html
• http://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html

External links from ACL2____GITHUB-COMMIT-CODE-USING-PULL-REQUESTS

• https://github.com/acl2/acl2
• https://github.com/acl2/acl2/commits/master

External links from ACL2____GITHUB-COMMIT-CODE-USING-PUSH

• https://github.com/acl2/acl2/

External links from ACL2____GIT-QUICK-START

• https://github.com/acl2/acl2
• https://github.com/acl2/acl2/wiki/ACL2-repo-git-tips

External links from ACL2____GENTLE-INTRODUCTION-TO-ACL2-PROGRAMMING

• https://www.cs.utexas.edu/users/moore/acl2

External links from ACL2____Functions_02for_02Manipulating_02these_02Objects

• images/res/tours/flying.gif
• images/res/tours/stack.gif

External links from ACL2____Free_02Variables_02in_02Top-Level_02Input

• images/res/tours/twarning.gif

External links from ACL2____FURTHER-INFORMATION-ON-REWRITING

• images/res/tours/twarning.gif

External links from ACL2____FREQUENTLY-ASKED-QUESTIONS-BY-NEWCOMERS

• http://www.cs.utexas.edu/users/moore/acl2/current/combined-manual/index.html
• images/res/tours/twarning.gif

External links from ACL2____FINDING-DOCUMENTATION

• http://www.cs.utexas.edu/users/moore/acl2/v8-6/combined-manual/index.html

External links from ACL2____Evaluating_02App_02on_02Sample_02Input

• images/res/tours/green-line.gif
• images/res/tours/walking.gif

External links from ACL2____EXAMPLE-INDUCTION-SCHEME-NAT-RECURSION

• images/res/tours/twarning.gif

External links from ACL2____DOUBLE-REWRITE

• http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.90.7190&rep=rep1&type=pdf
• http://portal.acm.org/toc.cfm?id=1217975

External links from ACL2____DOCUMENTATION-COPYRIGHT

• LICENSE

External links from COMMON-LISP____DOCUMENTATION

• download/
• http://www.cs.utexas.edu/users/moore/acl2
• http://www.cs.utexas.edu/users/moore/acl2/v8-6/combined-manual/index.html

External links from ACL2____DOC

• http://www.cs.utexas.edu/users/moore/acl2/v8-6/combined-manual/index.html

External links from ACL2____DF

• http://www.lispworks.com/documentation/lw71/CLHS/Body/v_featur.htm

External links from ACL2____DEFWARRANT

• http://www.cs.utexas.edu/users/kaufmann/papers/apply/index.html

External links from ACL2____DEFBADGE

• http://www.cs.utexas.edu/users/kaufmann/papers/apply/index.html

External links from ACL2____DEFABSSTOBJ

• http://www.cs.uwyo.edu/~ruben/acl2-13

External links from ACL2____Corroborating_02Models

• images/res/tours/flying.gif

External links from ACL2____Common_02Lisp

• https://www.cs.cmu.edu/Groups/AI/html/cltl/cltl2.html
• images/res/tours/twarning.gif
• images/res/tours/walking.gif

External links from ACL2____COURSE-MATERIALS

• http://dracula-lang.github.io/index.html
• http://www.cs.utexas.edu/users/hunt/class/index.html
• http://www.cs.utexas.edu/users/moore/classes/index.html
• http://www.cs.uwyo.edu/~cowles/jvm-acl2/
• https://www.ccs.neu.edu/home/pete/courses/Logic-and-Computation/2020-Spring/
• https://www.ccs.neu.edu/home/pete/teaching.html
• mailto:kaufmann@cs.utexas.edu
• mailto:moore@cs.utexas.edu

External links from ACL2____COMMUNITY-BOOKS

• http://www.cs.utexas.edu/users/moore/acl2/
• https://github.com/acl2/acl2/

External links from ACL2____COMMON-LISP

• http://www.lispworks.com/documentation/HyperSpec/Body/03_bbc.htm
• http://www.lispworks.com/documentation/HyperSpec/Front

External links from COMMON-LISP____COERCE

• http://www.cs.utexas.edu/users/moore/publications/km97a.pdf

External links from ACL2____CLAUSE-PROCESSOR

• http://ceur-ws.org/Vol-212/

External links from ACL2____CCL-INSTALLATION-MAC-ELABORATE

• https://github.com/Clozure/ccl/releases/

External links from ACL2____CCL-INSTALLATION-MAC-BRIEF

• https://github.com/Clozure/ccl/releases/

External links from ACL2____CCL-INSTALLATION-LINUX-ELABORATE

• https://github.com/Clozure/ccl/releases/

External links from ACL2____CCL-INSTALLATION-LINUX-BRIEF

• https://github.com/Clozure/ccl/releases/

External links from ACL2____CCL-INSTALLATION-EXTRA

• https://github.com/Clozure/ccl/releases/

External links from ACL2____CCL-INSTALLATION

• https://github.com/Clozure/ccl/releases

External links from ACL2____BUILDING-ACL2

• https://www.cs.utexas.edu/users/moore/acl2/current/HTML/installation/installation.html

External links from ACL2____BOOLE_42

• http://www.lispworks.com/documentation/HyperSpec/
• http://www.lispworks.com/documentation/HyperSpec/Body/f_boole.htm

External links from ACL2____BOOKS-CERTIFICATION-ALT

• http://www.cs.utexas.edu/users/moore/acl2/v8-6/HTML/installation/installation.html

External links from ACL2____BOOKS-CERTIFICATION

• download/
• http://www.cs.utexas.edu/users/moore/acl2/v8-6/HTML/installation/installation.html

External links from ACL2____BOOKS

• http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html#Books
• https://en.wikipedia.org/wiki/Source_code

External links from ACL2____BIBLIOGRAPHY

• http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html

External links from ACL2____BACKQUOTE

• http://www.lispworks.com/documentation/HyperSpec/Body/02_df.htm

External links from ACL2____An_02Example_02of_02ACL2_02in_02Use

• images/res/tours/walking.gif

External links from ACL2____An_02Example_02Common_02Lisp_02Function_02Definition

• images/res/tours/binary-trees-app.gif
• images/res/tours/binary-trees-x-y.gif
• images/res/tours/walking.gif

External links from ACL2____About_02the_02Prompt

• images/res/tours/twarning.gif

External links from ACL2____About_02the_02Admission_02of_02Recursive_02Definitions

• images/res/tours/twarning.gif

External links from ACL2____About_02the_02ACL2_02Home_02Page

• http://www.cs.utexas.edu/users/moore/acl2/
• https://www.cs.utexas.edu/users/moore/acl2/v8-6/acl2-doc.html#User's-Manual
• images/res/tours/flying.gif
• images/res/tours/twarning.gif

External links from ACL2____About_02Types

• images/res/tours/twarning.gif

External links from ACL2____About_02Models

• images/res/tours/computing-machine.gif
• images/res/tours/flying.gif

External links from ACL2____APPLY_42

• http://www.cs.utexas.edu/users/kaufmann/papers/apply/index.html

External links from ACL2____ANNOTATED-ACL2-SCRIPTS

• http://www.cs.utexas.edu/users/moore/acl2/contrib/POLISHING-PROOFS-TUTORIAL.html
• http://www.cs.utexas.edu/users/moore/publications/tutorial/kaufmann-TPHOLs08/index.html
• http://www.cs.utexas.edu/users/moore/publications/tutorial/rev3.html
• http://www.cs.utexas.edu/users/moore/publications/tutorial/sort-equivalence
• http://www.cs.utexas.edu/users/moore/publications/tutorial/sort-equivalence.tgz

External links from ACL2____ACL2-TUTORIAL

• http://tryacl2.org
• http://www.cs.utexas.edu/users/moore/acl2
• http://www.cs.utexas.edu/users/moore/publications/acl2-books/car/index.html

External links from ACL2____ACL2-HELP

• https://utlists.utexas.edu/sympa/info/acl2
• https://utlists.utexas.edu/sympa/info/acl2-help

External links from ACL2____ACL2-DOC

• http://www.cs.utexas.edu/users/moore/acl2/manuals/current/rendered-doc-combined.lsp.gz
• http://www.cs.utexas.edu/users/moore/acl2/v8-6/combined-manual/index.html
• https://github.com/acl2/acl2/

External links from ACL2____ACL2_02is_02an_02Untyped_02Language

• images/res/tours/twarning.gif

External links from ACL2____ACL2_02as_02an_02Interactive_02Theorem_02Prover_02_82cont_92

• images/res/tours/twarning.gif
• images/res/tours/walking.gif

External links from ACL2____ACL2_02as_02an_02Interactive_02Theorem_02Prover

• images/res/tours/interactive-theorem-prover.gif

External links from ACL2____ACL2_02System_02Architecture

• images/res/tours/acl2-system-architecture.gif
• images/res/tours/twarning.gif
• images/res/tours/walking.gif

External links from ACL2____ACL2_02Symbols

• images/res/tours/twarning.gif

External links from ACL2____ACL2_02Strings

• images/res/tours/twarning.gif

External links from ACL2____ACL2_02Conses_02or_02Ordered_02Pairs

• images/res/tours/twarning.gif

External links from ACL2____ACL2_02Characters

• images/res/tours/twarning.gif

External links from ACL2____ACKNOWLEDGMENTS

• https://github.com/acl2/acl2/

External links from ACL2____ABOUT-ACL2

• http://www.cs.utexas.edu/users/moore/acl2/

External links from ACL2____A_02Walking_02Tour_02of_02ACL2

• images/res/tours/large-walking.gif
• images/res/tours/twarning.gif
• images/res/tours/walking.gif

External links from ACL2____A_02Typical_02State

• images/res/tours/flying.gif
• images/res/tours/state-object.gif

External links from ACL2____A_02Trivial_02Proof

• images/res/tours/concrete-proof.gif

External links from ACL2____A_02Tiny_02Warning_02Sign

• images/res/tours/twarning.gif
• images/res/tours/warning.gif

External links from ACL2____A_02Sketch_02of_02How_02the_02Rewriter_02Works

• images/res/tours/uaa-rewrite.gif

External links from ACL2____A_02Flying_02Tour_02of_02ACL2

• images/res/tours/flying.gif
• images/res/tours/large-flying.gif

External links from ACL2_____A2COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE_A2

• http://dx.doi.org/10.1145/147135.147249