Formal categorical reasoning

DOI10.55730/1300-0098.3178OpenAlexW4285138336MaRDI QIDQ5102205FDOQ5102205

Authors: Burak Ekici 

Publication date: 6 September 2022

Published in: Turkish Journal of Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.55730/1300-0098.3178

Recommendations

• scientific article; zbMATH DE number 4202247
• Abstract categorical logic
• scientific article; zbMATH DE number 1554269
• A formal logic for formal category theory
• A categorial type logic
• Categorical properties of logical frameworks
• Categorial inference and modal logic
• scientific article; zbMATH DE number 2232835
• Logic in category theory
• scientific article; zbMATH DE number 733385

zbMATH Keywords

categorical logicCoq proof assistantformal proofsdenotational semantics of programming constructs

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Title not available (Why is that?)
• Notions of computation and monads
• Title not available (Why is that?)
• Title not available (Why is that?)
• Combinators and functional programming languages. Thirteenth Spring School of the LITP, Val d'Ajol, France, May 6-10, 1985. Proceedings
• Higher order unification via explicit substitutions
• Experience implementing a performant category-theory library in Coq
• Category theory in Coq 8.5
• Computer Aided Systems Theory – EUROCAST 2005

Cited In (3)

• A comparison of HOL and ALF formalizations of a categorical coherence theorem
• CatTheo
• Category theory in Isabelle/HOL as a basis for meta-logical investigation

Uses Software

• Coq

This page was built for publication: Formal categorical reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5102205)