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 → plclub → Metalib

plclub / Metalib

Licence: other
The Penn Locally Nameless Metatheory Library

Labels

coq

Projects that are alternatives of or similar to Metalib

Software Foundations
Solutions to the exercises from the 'Software Foundations' book by Benjamin Pierce et al.
Stars: ✭ 9 (-80.85%)
Mutual labels:  coq
Coq Printf
Implementation of sprintf for Coq
Stars: ✭ 15 (-68.09%)
Mutual labels:  coq
Parseque
Total Parser Combinators in Coq
Stars: ✭ 37 (-21.28%)
Mutual labels:  coq
Coqjvm
Coq executable semantics and resource verifier
Stars: ✭ 10 (-78.72%)
Mutual labels:  coq
Hello World
A Hello World program in Coq.
Stars: ✭ 14 (-70.21%)
Mutual labels:  coq
Profunctor Monad
Bidirectional programming in Haskell with monadic profunctors
Stars: ✭ 30 (-36.17%)
Mutual labels:  coq
Hott Species
Combinatorial species in HoTT
Stars: ✭ 9 (-80.85%)
Mutual labels:  coq
Pornview
Porn browser formally-verified in Coq
Stars: ✭ 42 (-10.64%)
Mutual labels:  coq
Vvclocks
Verified vector clocks, with Coq!
Stars: ✭ 14 (-70.21%)
Mutual labels:  coq
Compcert
The CompCert formally-verified C compiler
Stars: ✭ 984 (+1993.62%)
Mutual labels:  coq
Stalin Sort
Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️
Stars: ✭ 868 (+1746.81%)
Mutual labels:  coq
Jt89
sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility
Stars: ✭ 14 (-70.21%)
Mutual labels:  coq
Nuprlincoq
Implementation of Nuprl's type theory in Coq
Stars: ✭ 31 (-34.04%)
Mutual labels:  coq
Dblib Linear
Formalisation of the linear lambda calculus in Coq
Stars: ✭ 10 (-78.72%)
Mutual labels:  coq
Certint
A Certified Interpreter for ML with Structural Polymorphism
Stars: ✭ 39 (-17.02%)
Mutual labels:  coq
Monads
Coq code accompanying several articles on semantics of functional programming languages
Stars: ✭ 9 (-80.85%)
Mutual labels:  coq
Hott
Homotopy type theory
Stars: ✭ 946 (+1912.77%)
Mutual labels:  coq
Poleiro
A blog about Coq
Stars: ✭ 42 (-10.64%)
Mutual labels:  coq
Freespec
A framework for implementing and certifying impure computations in Coq
Stars: ✭ 41 (-12.77%)
Mutual labels:  coq
Paramcoq
Coq plugin for parametricity [[email protected]]
Stars: ✭ 32 (-31.91%)
Mutual labels:  coq
View All Similar Projects ➔

COMPILATION, INSTALLATION, AND DOCUMENTATION:

This library requires Coq 8.10, available via opam or from the Coq website [https://coq.inria.fr/download].

To compile the library, cd to the Metalib directory:

`make`          generate Coq makefile, compile Coq files
  `make html`     generate Coq documentation
  `make install`  install library on your system (locally)

Note that both step 1 and 3 are needed in order to be able to run/compile the examples and the tutorial. In particular, step 3 only install the library in your local Coq setup, and does not require special privileges.

The main documentation for this library is available as a collection of HTML files.

TUTORIAL:

The metatheory library comes with a tutorial in directory Stlc. Make sure that you've compiled the library first. These tutorial files contains an introduction to mechanizing programming language definitions with binding in Coq and how to reason about them.

An additional example of the library is available in the Fsub directory.

Those new to Coq should start with Software Foundations, which is an introduction to using Coq. The tutorial assumes some familarity with this resource. (https://softwarefoundations.cis.upenn.edu/current/index.html)

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].