PL
a dialect of The Monkey Programming Language
Rust mid-level IR Abstract Interpreter
Lecture notes for a short course on proving/programming in Coq via SSReflect.
The Rosette solver-aided host language, sample solver-aided DSLs, and demos
A static verifier for Rust, based on the Viper verification infrastructure.
“连续八年成为全世界最受喜爱的语言，无 GC 也无需手动内存管理、极高的性能和安全性、过程/OO/函数式编程、优秀的包管理、JS 未来基石" — 工作之余的第二语言来试试 Rust 吧。本书拥有全面且深入的讲解、生动贴切的示例、德芙般丝滑的内容，这可能是目前最用心的 Rust 中文学习教程 / Book
Learn Rust dark magics by implementing an expression framework in database systems
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…
The core OCaml system: compilers, runtime system, base libraries
Language for high-assurance and high-speed cryptography
A free book about developing secure and robust systems software.
10 papers that all PhD students in programming languages ought to know, for some value of 10
Blazing fast and correct x86/x64 disassembler, assembler, decoder, encoder for Rust, .NET, Java, Python, Lua
Probabilistic language based on pattern matching and constraint propagation, 153 examples
Formal specification and verification of hardware, especially for security and privacy.
Creusot helps you prove your code is correct in an automated fashion.
Coq to Rust program extraction. The whole tree is on the original Coq code base.
Tricks you wish the Coq manual told you [maintainer=@tchajed]