The goal of the Ynot project is to make programming with dependent types practical for a modern programming language. In particular, we are extending the Coq proof assistant to make it possible to write higher-order, imperative and concurrent programs (in the style of Haskell) through a shallow embedding of Hoare Type Theory (HTT). HTT provides a clean separation between pure and effectful computations, makes it possible to formally specify and reason about effects, and is fully compositional. more...
linked to me from https://twitter.com/cattheory/status/1220803662802489344 (by Joomy Korkut, PhD student in programming languages at Princeton https://cs.princeton.edu/~ckorkut/) — « not a language but a way to reason about C programs in Coq: VST lets you define separation logic predicates that describe how a Coq type would be represented in C: https://cs.princeton.edu/~appel/vc/Verif_reverse.html#lab32 \n\n might be interesting to you, or not, I don't know. » at 9:20 PM CET on Jan 24, 2020
The goal of the Ynot project is to make programming with dependent types practical for a modern programming language. In particular, we are extending the Coq proof assistant to make it possible to write higher-order, imperative and concurrent programs (in the style of Haskell) through a shallow embedding of Hoare Type Theory (HTT). HTT provides a clean separation between pure and effectful computations, makes it possible to formally specify and reason about effects, and is fully compositional. This seems like it's related to Adam Chlipala's A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. See, in particular, slides 23-24 of this presentation (PDF). More generally, computation and reflection seem to be gaining recognition as important features for the practical use of Coq Again, the point is to simplify programming with dependent types in Coq
CiME 3 is a rewriting toolbox that provides Coq certificates for termination proofs (standard rewriting) obtained using various criteria: * Dependency pairs: o plain/marks, o graphs refinements with or without sub-term criterion, as well as various orderings: * Polynomial interpretations, * Matrix interpretations, * Full RPO with status, with AFS refinements. CiME 3 may be used alone (searching for proofs and producing certificates) or in conjunction with your own prover via xml input/output and translation to .v files. Note that in addition to its own xml format, CiME 3 now supports CPF for the aformentioned techniques.
ProofWeb is a system for practising natural deduction on the computer based on the Coq proof assistant and runs in browser. ProofWeb one runs logic exercises on a web server. ProofWeb comes with a database of basic logic exercises that are graded according to difficulty. The ProofWeb system automatically grades the exercises of the students. user talks to the Coq system on the server without any translation. There just are a few additional tactics to make Coq's behavior follow the logic textbooks. This means that in ProofWeb the full power of Coq is available, even to beginner students. On the other hand ProofWeb tries hard to present deductions exactly the way they look in the textbooks. In particular ProofWeb exactly follows the conventions of a well-known logic textbook Logic in Computer Science: Modelling and Reasoning about Systems by Michael Huth and Mark Ryan.
Russell is a language for programming with dependent types in Coq. It uses an adaptation of the predicate subtyping feature of PVS to allow users to write only algorithmic code while using strong specifications. Proof obligations are generated automatically, and, once proved, permit to build a complete, valid Coq term. As an example of using Russell to develop programs with dependent types, I implemented the Finger Tree data structure [3] in Coq. It gives quite a few insights about the power of dependent types for specification and their practical use [4]. Here's the relevant page. You can have a look at the example on celebrities in a party inspired by Richard Bird's article. Yet a lighter example: quicksort. I developed a complete formalization [5] of simply-typed lambda calculus with constants in the dependently-typed style with the help of Program. It includes a tait-style proof of weak normalization.
R. Dapoigny, and P. Barlatier. Proceedings of the 21th International Conference on Conceptual Structures (ICCS 2013), volume 7735 of Lecture Notes in Computer Science, page 135-152. Springer, (2013)