Publication

Camltac: OCaml as a Tactic Language

2026

Résumé

We present Camltac, a Rocq plugin that allows OCaml to be written directly within Rocq scripts. Camltac blurs the line between Rocq plugins and tactics, letting users leverage the expressivity, performance, and rich ecosystem of OCaml to write tactics and meta-programs, without compromising on simplicity and convenience.

Source officielle

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

2026

Résumé

Source officielle

Concepts associés (26)

Coq (logiciel)

Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe PI.R2 de l’Inria au sein du laboratoire PPS du CNRS et en partenariat avec l'École polytechnique, le CNAM, l'Université Paris Diderot et l'Université Paris-Sud (et antérieurement l'École normale supérieure de Lyon). Le nom du logiciel (initialement CoC) est particulièrement adéquat car : il est français ; il est fondé sur le calcul des constructions (CoC abrégé en anglais) introduit par Thierry Coquand.

Agda (programming language)

Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version, originally known as Agda 2, is a full rewrite, which should be considered a new language that shares a name and tradition. Agda is also a proof assistant based on the propositions-as-types paradigm, but unlike Coq, has no separate tactics language, and proofs are written in a functional programming style.

OCaml

OCaml, anciennement connu sous le nom d'Objective Caml, est l'implémentation la plus avancée du langage de programmation Caml, créé par Xavier Leroy, Jérôme Vouillon, , Didier Rémy et leurs collaborateurs en 1996. Ce langage, de la famille des langages ML, est un projet open source dirigé et maintenu essentiellement par l'Inria. OCaml est le successeur de Caml Light, auquel il a ajouté entre autres une couche de programmation objet.

Afficher plus

Publications associées (4)

Afficher plus

Camltac: OCaml as a Tactic Language

Chattez avec Graph Search

Investigating the impact of nitrogen deposition on the emergent forest ecosystem

On the Evaluation and Real-World Usage Scenarios of Deep Vessel Segmentation for Funduscopy

Grouping trumps pooling and centroids in crowding