はてなブックマーク

Stacked Borrows An Aliasing Model for Rust Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, Derek Dreyer. POPL 2020. Paper Talk at POPL Technical Appendix Coq Formalization Artifact (with VM) Type systems are useful not just for the safety guarantees they provide, but also for helping compilers generate more efficient code by simplifying important program analyses. In Rust, the type system imposes a stric

Update The ERC-funded RustBelt project has now formally ended (as of April 2021), but the project continues in spirit, and we continue to seek exceptional candidates for PhD and postdoc positions at MPI-SWS. We look forward to continued exploration of Rust, Iris, separation logic, relaxed memory models, and more. See below for information on how to apply. Original announcement We are very pleased

2014 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014) Module systems like that of Haskell permit only a weak form of modularity in which module implementations directly depend on other implementations and must be processed in dependency order. Module systems like that of ML, on the other hand, permit a stronger form of modularity in which explicit interfaces express

Paco is a Coq library implementing parameterized coinduction. Parameterized coinduction is a technique for defining coinductive predicates (i.e., in Prop), using which one can perform coinductive proofs in a more compositional and incremental fashion than with standard Tarski-style constructions. The Paco library provides a tactic called "pcofix", replacing Coq's primitive cofix and avoiding its s