Tag: Rocq
-
Discussing “The MetaCoq Project”
I’ve written before about Coq, recently renamed to Rocq, a proof assistant based on Martin-Löf’s dependent type theory. This paper, along with various sequels written in the six years since the project was first announced, aims to mechanise the syntax and semantics of Rocq, in Rocq.
-
Discussing “Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions”
I’ve written before about the Coq Proof Assistant . Since then, after years of bravely ignoring the sniggers its French name produced among English speakers, the developers have decided to remain it Rocq in honour of Rocquencourt, the French town in which much of the development took place. The good news for the authors of…
Categories
Recent Posts
- Discussing “Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic”
- Discussing “Basic Proof Theory”
- A Blog Update for 2025
- Discussing “Proof Analysis in Modal Logic”
Tags
1996 2000 2001 2014 2019 2020 2021 2023 Abhishek Anand Cambridge Tracts in Theoretical Computer Science Carnegie Mellon University City University of New York Coq Cubical Type Theory Cyril Cohen Fabian Kunze intuitionistic logic intuitionistic modal logic Jonathan Sterling Journal of Automated Reasoning LICS LORIA Maarten de Rijke Matthieu Sozeau Melvin Fitting Metaprogramming modal logic nested sequent calculus Notre Dame Journal of Formal Logic Patrick Blackburn Princeton University Proof theory Rocq sequent calculus Simon Boulier TABLEAUX types type theory University of Amsterdam University of Birmingham University of Cambridge University of Oxford Valeria de Paiva Yannick Forster Yde Venema