λProlog and the Calculus of Inductive Constructions (original) (raw)

Skip to content

Navigation Menu

• • AI CODE CREATION
    * GitHub CopilotWrite better code with AI
    * GitHub SparkBuild and deploy intelligent apps
    * GitHub ModelsManage and compare prompts
    * MCP RegistryNewIntegrate external tools

View all features

• Pricing

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Sign up

Appearance settings

Let's boost λProlog to implement an elaborator for CIC!

• Overview
• Repositories
• Projects
• Packages
• People

Pinned Loading

1. Embeddable Lambda Prolog Interpreter
   Prolog 332 43
2. Coq plugin embedding elpi
   Rocq Prover 177 69

Repositories

Type

Select type

All Public Sources Forks Archived Mirrors Templates

Language

Select language

All HTML JavaScript OCaml Prolog Rocq Prover

Sort

Select order

Last updated Name Stars

Showing 6 of 6 repositories

• coq-elpi Public
  Coq plugin embedding elpi
  LPCIC/coq-elpi’s past year of commit activity
  Rocq Prover
  177
  LGPL-2.1
  69 83 25
  Updated Dec 17, 2025
• elpi Public
  Embeddable Lambda Prolog Interpreter
  LPCIC/elpi’s past year of commit activity
  Prolog
  332
  LGPL-2.1
  43 38 14
  Updated Dec 12, 2025
• elpi-lang Public
  visual studio code extension for Elpi
  LPCIC/elpi-lang’s past year of commit activity
  JavaScript
  7
  MIT
  1 8 3
  Updated Nov 15, 2025
• LPCIC/coq-elpi-lang’s past year of commit activity
  3
  MIT 0
  1 0
  Updated Nov 4, 2025
• LPCIC/coq-elpi-www’s past year of commit activity
  HTML 0 0
  0 0
  Updated Oct 17, 2018
• matita Public archive
  Matita (proof assistant) with embedded elpi
  LPCIC/matita’s past year of commit activity
  OCaml
  14 3 3 0
  Updated Jan 30, 2018

People

This organization has no public members. You must be a member to see who’s a part of this organization.

Most used topics