GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → siegebell → Vscoq

siegebell / Vscoq

Licence: other
Coq Support for Visual Studio Code

Programming Languages

typescript
32286 projects

Labels

coq

Projects that are alternatives of or similar to Vscoq

Parseque
Total Parser Combinators in Coq
Stars: ✭ 37 (-56.47%)
Mutual labels:  coq
Perennial
Verifying concurrent crash-safe systems
Stars: ✭ 57 (-32.94%)
Mutual labels:  coq
Certicoq
A Verified Compiler for Gallina, Written in Gallina
Stars: ✭ 66 (-22.35%)
Mutual labels:  coq
Freespec
A framework for implementing and certifying impure computations in Coq
Stars: ✭ 41 (-51.76%)
Mutual labels:  coq
Silveroak
Formal specification and verification of hardware, especially for security and privacy.
Stars: ✭ 51 (-40%)
Mutual labels:  coq
Collapsing Towers
Collapsing Towers of Interpreters
Stars: ✭ 61 (-28.24%)
Mutual labels:  coq
Paramcoq
Coq plugin for parametricity [[email protected]]
Stars: ✭ 32 (-62.35%)
Mutual labels:  coq
Disel
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Stars: ✭ 85 (+0%)
Mutual labels:  coq
Verlang
Stars: ✭ 52 (-38.82%)
Mutual labels:  coq
Sfja
SoftwareFoundations(Ja)
Stars: ✭ 65 (-23.53%)
Mutual labels:  coq
Pornview
Porn browser formally-verified in Coq
Stars: ✭ 42 (-50.59%)
Mutual labels:  coq
Metalib
The Penn Locally Nameless Metatheory Library
Stars: ✭ 47 (-44.71%)
Mutual labels:  coq
Riscv Coq
RISC-V Specification in Coq
Stars: ✭ 63 (-25.88%)
Mutual labels:  coq
Certint
A Certified Interpreter for ML with Structural Polymorphism
Stars: ✭ 39 (-54.12%)
Mutual labels:  coq
Formal Type Theory
Formalising Type Theory in a modular way for translations between type theories
Stars: ✭ 74 (-12.94%)
Mutual labels:  coq
Compcert
The CompCert formally-verified C compiler
Stars: ✭ 984 (+1057.65%)
Mutual labels:  coq
Scala Escape
A compiler plug-in to control object lifetimes in Scala
Stars: ✭ 60 (-29.41%)
Mutual labels:  coq
Typetheory
The mathematical study of type theories, in univalent foundations
Stars: ✭ 86 (+1.18%)
Mutual labels:  coq
Ch2o
Stars: ✭ 75 (-11.76%)
Mutual labels:  coq
Scallina
A Coq-based synthesis of Scala programs which are correct-by-construction
Stars: ✭ 65 (-23.53%)
Mutual labels:  coq
View All Similar Projects ➔

A plugin for the Coq Proof Assistant 8.5 and 8.6 in Visual Studio Code.

Features

  • Asynchronous proofs
  • Syntax highlighting
  • Commands: step forward, interpret to point, interrupt computation, queries, set display options, etc.
  • Diff view for proof-view: highlight which terms change between states
  • Smarter editing: does not roll back the state when editing whitespace or comments
  • Works with prettify-symbols-mode
  • Supports _CoqProject
  • The proof-view can be opened in an external web browser
  • LtacProf results treeview

Screenshots

Simple example Screenshot of Proof Goal

LtacProfiling view:
Simple example

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].