@arialdo what's the problem being observed? Though it's a normal example case in automatic proof assistants like #acl2 how it can take hundreds of steps to sketch
(thm
(implies (and (true-listp list) (equal rrlist (rev (rev list))))
(equal rrlist list)))

Verified implementation of an efficient term-rewriting algorithm for multiplier verification on ACL2. ~ Mertcan Temel. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL22022.11.pdf #ITP #ACL2

A formalization of finite group theory. ~ David M. Russinoff. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL22022.10.pdf #ITP #ACL2

Modeling asymptotic complexity using ACL2. ~ William D. Young. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL22022.9.pdf #ITP #ACL2

A free group of rotations of rank 2. ~ Jagadish Bapanapally, Ruben Gamboa. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL22022.8.pdf #ITP #ACL2 #Math

A mechanized proof of bounded convergence time for the distributed perimeter surveillance system (DPSS) algorithm. ~ David Greve, Jennifer Davis, Laura Humphrey. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL22022.5.pdf #ITP #ACL2

Using ACL2 to teach students about software testing. ~ Ruben Gamboa, Alicia Thoney. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL22022.4.pdf #ITP #ACL2

All prime numbers have primitive roots. ~ Ruben Gamboa, Woodrow Gamboa. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL22022.3.pdf #ITP #ACL2 #Math

Calculational proofs in ACL2s. ~ Andrew T. Walter, Ankit Kumar, Panagiotis Manolios. https://arxiv.org/abs/2307.12224 #ITP #ACL2 #Logic

Why is there no #ACL2 mode in #Emacs?

@awkravchuk @rwxrwxrwx
#acl2 defines #'+ as a macro like this:
(defmacro + (&rest rst)
(if rst (if (cdr rst) (xxxjoin 'binary-+ rst)
(cons 'binary-+ (cons 0 (cons (car rst) nil))))
0))
where 'binary-+ adds/guards two number arguments. So I guess there's that (+) -> 0 again ;p

A formal analysis of Karn’s algorithm. ~ Max von Hippel, Kenneth L. McMillan, Cristina Nita-Rotaru, Lenore D. Zuck. https://cnitarot.github.io/papers/rtt_netys2023.pdf #ITP #ACL2

Formalizations of the Tonelli-Shanks algorithm in ACL2, integration by substitution and the Banach-Tarski theorem in ACL2(r). ~ Jagadish Bapanapally. https://www.proquest.com/openview/1c86fe582160dae130ec4cd4129de8f8/1?pq-origsite=gscholar&cbl=18750&diss=y #PhDThesis #ITP #ACL2 #Math 

@dekkzz76 what are your #prolog hopes and dreams? @pizzapal is an #swiprolog game programmer amoungst many virtues. Asking me to not write in #CommonLisp / #ACL2 / #interlisp / #elisp is abstruse.

@Jose_A_Alonso [my friend mentioned this to me]
@dekkzz76 this is a very attractive, powerful and obviously useful approach to programming [linked notes, PAIP, every lisp programmer and compiler]. The reason I use #CommonLisp and #ACL2 is that in prolog, I would often like to build infrastructure up to the point where I've implemented half of common lisp. Even for proofs [ACL2 when prolog was also very widely used like this].
So I would prolog in lisp, rather than putting #ECL in #SWIProlog eg

Interesting: https://github.com/acl2/acl2/tree/master/books/rtl

"This directory contains an ACL2 library of register-transfer logic, developed at #AMD from 1995 to 2011, at #Intel from 2012 to 2016, and at #Arm from 2016 to the present, in support of the mechanical verification of floating-point arithmetic units designed during those periods by the respective companies."

For those who don't know, #ACL2 is a theorem prover in #CommonLisp.

#Lisp #FormalVerification #RTL #HardwareEngineering #Semiconductors

Interesting: https://github.com/acl2/acl2/tree/master/books/rtl

"This directory contains an ACL2 library of register-transfer logic, developed at #AMD from 1995 to 2011, at #Intel from 2012 to 2016, and at #Arm from 2016 to the present, in support of the mechanical verification of floating-point arithmetic units designed during those periods by the respective companies."

For those who don't know, #ACL2 is a theorem prover in #CommonLisp.

#Lisp #FormalVerifcation #RTL #HardwareEngineering #Semiconductors

Last week for the early registration to the European Lisp Symposium, See you in Amsterdam!

https://www.european-lisp-symposium.org/2023

#lisp @commonlisp @scheme @racket @lisp_discussions @DylanLang #commonlisp #scheme #elisp #dylanlang #racket #acl2

Dear Lispers of all dialects,

did you notice the keynote talks and speakers for the next ELS2023:

⭐​ "Gradual, Multi-Lingual, and Teacher-Centric Programming Education" 🔸 ​Felienne Hermans 🔸 Vrije Universiteit Amsterdam, Nederlands

⭐​ "Artificial Intelligence: a Problem of Plumbing?" 🔸 Gerald J. Sussman 🔸 MIT CSAIL, USA

🤩​🤩​

https://www.european-lisp-symposium.org/2023/index.html

@lisp @commonlisp @scheme @racket #lisp #commonlisp #emacslisp #racket #dylanlang #acl2 #scheme
🎉​

Dear Lispers of all dialects,

did you notice the keynote talks and speakers for the next ELS2023:

⭐​ "Gradual, Multi-Lingual, and Teacher-Centric Programming Education" 🔸​Felienne Hermans 🔸​ Vrije Universiteit Amsterdam, Nederlands

⭐​ Artificial Intelligence: a Problem of Plumbing? 🔸Gerald J. Sussman 🔸MIT CSAIL, USA

🤩​

https://www.european-lisp-symposium.org/2023/index.html

@lisp @commonlisp @scheme @racket #lisp #commonlisp #emacslisp #racket #dylanlang #acl2 #scheme
🎉​