Programming Languages
22,586 items in 77 lists
-
Whenever dangermouse.net
Language that does things whenever it wants.
-
Piet dangermouse.net
Language in which programs look like abstract paintings using colors as code. Named after Piet Mondrian.
-
Petrovich dangermouse.net
Operating System concept based on random actions and rewards/punishments.
-
Ook! dangermouse.net
Brainfuck-based language, where the commands are orangutan words.
-
Haifu dangermouse.net
Designed with the core values of Eastern philosophy in mind.
-
Chef dangermouse.net
Programs that look like cooking recipes.
-
DM's Esoteric Programming Languages dangermouse.net
List of esoteric languages and algorithms written by dangermouse.
-
Code Golf Stack Exchange codegolf.stackexchange.com
Golfing problems and answers.
-
INTERCAL catb.org
Parody language intended to be completely different from other languages.
-
On the Turing Completeness Of MS PowerPoint andrew.cmu.edu
Turing Machine on PowerPoint.
-
Coq keyword on Zenodo zenodo.org
-
Official Coq X/Twitter x.com
-
VST vst.cs.princeton.edu
Toolchain for verifying C code inside Coq in a higher-order concurrent, impredicative separation logic that is sound w.r.t. the Clight language of the CompCert compiler.
-
Vélus velus.inria.fr
Verified compiler for a Lustre/Scade-like dataflow synchronous language.
-
Proofs and Reliable Programming using Coq team.inria.fr
Introduction to developing and verifying programs with Coq.
-
Official Coq-Club mailing list sympa.inria.fr
-
An Introduction to MathComp-Analysis staff.aist.go.jp
Lecture notes on getting started with the Mathematical Components library and using it for classical reasoning and real analysis.
-
Coq tag on Stack Overflow stackoverflow.com
-
Volume 3: Verified Functional Algorithms softwarefoundations.cis.upenn.edu
Demonstration of how a variety of fundamental data structures can be specified and verified.
-
Volume 5: Verifiable C softwarefoundations.cis.upenn.edu
An extended tutorial on specifying and verifying C programs using the Verified Software Toolchain.
-
Volume 6: Separation Logic Foundations softwarefoundations.cis.upenn.edu
An introduction to separation logic and how to build program verification tools on top of it.
-
Volume 4: QuickChick softwarefoundations.cis.upenn.edu
Introduction to tools for combining randomized property-based testing with formal specification and proof.
-
Volume 2: Programming Language Foundations softwarefoundations.cis.upenn.edu
Introduction to the theory of programming languages, including operational semantics, Hoare logic, and static type systems.
-
Volume 1: Logical Foundations softwarefoundations.cis.upenn.edu
Introduction to functional programming, basic concepts of logic, and computer-assisted theorem proving.
-
Thomas Letan's blog posts on Coq soap.coffee
-
Hybrid site.uottawa.ca
System for reasoning using higher-order abstract syntax representations of object logics.
-
PLClub Blog seas.upenn.edu
-
Nix Coq packages search.nixos.org
Collection of Coq-related packages for Nix.
-
Computer Arithmetic and Formal Proofs sciencedirect.com
Book that describes how to formally specify and verify floating-point algorithms in Coq using the Flocq library.
-
Coq subreddit reddit.com
-
Ralf Jung's blog posts on Coq ralfj.de
-
Proof General proofgeneral.github.io
Generic interface for proof assistants based on the extensible, customizable text editor Emacs.
-
Coq tag on Proof Assistants Stack Exchange proofassistants.stackexchange.com
-
Coq Exchange: ideas and experiment reports about Coq project.inria.fr
-
Poleiro: a Coq blog by Arthur Azevedo de Amorim poleiro.info
-
Paco plv.mpi-sws.org
Library for parameterized coinduction.
-
MIT PLV blog posts on Coq plv.csail.mit.edu
-
Debian Coq packages people.debian.org
Coq-related packages available in the testing distribution of Debian.
-
opam opam.ocaml.org
Flexible and Git-friendly package manager for OCaml and Coq with multiple compiler support.
-
Mike Nahas's Coq Tutorial mdnahas.github.io
Basics of using Coq to write formal proofs.
-
The Mathematical Components book math-comp.github.io
Book oriented towards mathematically inclined users, focusing on the Mathematical Components library and the SSReflect proof language.
-
Learn X in Y minutes where X=Coq learnxinyminutes.com
Whirlwind tour of Coq as a language.
-
Coq'Art labri.fr
The first book dedicated to Coq.
-
Joachim Breitner's blog posts on Coq joachim-breitner.de
-
Iris iris-project.org
Higher-order concurrent separation logic framework.
-
Coq requirements in Common Criteria evaluations inria.hal.science
Guide on how to write readable and reviewable Coq code in high assurance applications.
-
Programs and Proofs ilyasergey.net
Book that gives a brief and practically-oriented introduction to interactive proofs in Coq which emphasizes the computational nature of inductive reasoning about decidable propositions via a small set of primitives from the SSReflect proof language.
-
Gregory Malecha's blog gmalecha.github.io
-
Program verification with types and logic gitlab.science.ru.nl
Lectures and exercise material for a course in programming language semantics, type systems and program logics, using Coq, at Radboud University Nijmegen.
-
Coq-std++ gitlab.mpi-sws.org
Extended alternative standard library for Coq.
- next page of items loading…
