Category Theory in Coq 8.5

Timany, Amin ; Jacobs, Bart

Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany, 2016

Online unknown

Zugriff:

We report on our experience implementing category theory in Coq 8.5. The repository of this development can be found at https://bitbucket.org/amintimany/categories/. This implementation most notably makes use of features, primitive projections for records and universe polymorphism that are new to Coq 8.5.

Comment: This is the abstract for a talk accepted for a presentation at the 7th Coq Workshop, Sophia Antipolis, France on June 26, 2015

Titel:	Category Theory in Coq 8.5
Autor/in / Beteiligte Person:	Timany, Amin ; Jacobs, Bart
Link:	View record in OpenAIRE (Volltext)
Veröffentlichung:	Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany, 2016
Medientyp:	unknown
DOI:	10.4230/lipics.fscd.2016.30
Schlagwort:	FOS: Computer and information sciences Computer Science - Logic in Computer Science 000 Computer science, knowledge, general works TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science Universe Polymorphism Category Theory Coq 8.5 Logic in Computer Science (cs.LO)
Sonstiges:	Nachgewiesen in: OpenAIRE Sprachen: English File Description: application/pdf Language: English Rights: OPEN

Klicken Sie ein Format an und speichern Sie dann die Daten oder geben Sie eine Empfänger-Adresse ein und lassen Sie sich per Email zusenden.

BibTeX Citavi, JabRef, u.a.
(Literaturverwaltung)

PDF kein Volltext!
(Merkzettel, Notizen)

RIS Endnote, Citavi u.a.
(Literaturverwaltung)

MODS
(XML zur Weiterverarbeitung)

oder

Wählen Sie das für Sie passende Zitationsformat und kopieren Sie es dann in die Zwischenablage, lassen es sich per Mail zusenden oder speichern es als PDF-Datei.

Gewünschter Zitations-Stil:

oder

Bitte prüfen Sie, ob die Zitation formal korrekt ist, bevor Sie sie in einer Arbeit verwenden. Benutzen Sie gegebenenfalls den "Exportieren"-Dialog, wenn Sie ein Literaturverwaltungsprogramm verwenden und die Zitat-Angaben selbst formatieren wollen.