*Agda builds on similar grounds as things like Coq, Minlog, even ACL2 and Isabel...

		Q6T46nT668w6i3m on Dec 1, 2014 \| parent \| context \| favorite \| on: Great Works in Programming Languages (2004) Agda builds on similar grounds as things like Coq, Minlog, even ACL2 and Isabelle, which are very old. … Coq, Minlog, even ACL2 and Isabelle build on similar grounds as Chrysippus’ in the 3rd century BC … i.e. there’s nothing new under the sun.