4 ms·
A few: * Fault Location via Dynamic Slicing * Interprocedural Analysis and the Verification of Concurrent Programs * Logics and Algorithms for Software Model
by Q6T46nT668w6i3m 12y ago
A few:
* Fault Location via Dynamic Slicing
* Interprocedural Analysis and the Verification of Concurrent Programs
* Logics and Algorithms for Software Model Checking
* Verifying Low-Level Programs via Liquid Type Inference
Moreover:
* Agda
* LLVM
- namarkiv 12y agoDependent types, gradual typing, HoTT
- sklogic 12y agoThanks! Interesting. I'll try to dig out the recent papers. Although I have a feeling that most of this is not that new. LLVM is just a very basic SSA, which is early 90s. Agda builds on similar grounds as things like Coq, Minlog, even ACL2 and Isabelle, which are very old. There've been a lot of buzz in the concurrent code verification ever since the early pi-calculus papers by R. Milner. But the liquid type inference seems to be a genuinely new thing, and apparently I totally missed it somehow. It even seems like I unknowingly reinvented something similar, by using arbitrary Prolog code as type attributes on top of a basic Hindley-Milner.
- Q6T46nT668w6i3m 12y agoAgda 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.
- tel 12y agoHoTT?