Types for Proofs and Programs

DOI10.1007/11617990zbMath1172.68623OpenAlexW4300050167MaRDI QIDQ5898170

Claudio Sacerdoti Coen, Stefano Zacchiroli, Andrea Asperti, Ferruccio Guidi, Enrico Tassi

Publication date: 13 November 2006

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11617990

Mathematics Subject Classification ID

Theory of languages and software systems (knowledge-based systems, expert systems, etc.) for artificial intelligence (68T35) Information storage and retrieval of data (68P20)

Related Items (12)

Classification of alignments between concepts of formal mathematical systems ⋮ A survey on retrieval of mathematical knowledge ⋮ Crystal: Integrating structured queries into a tactic language ⋮ Recycling proof patterns in Coq: case studies ⋮ User interaction with the Matita proof assistant ⋮ Integrating searching and authoring in Mizar ⋮ A User Interface for a Mathematical System that Allows Ambiguous Formulae ⋮ An Interactive Driver for Goal-directed Proof Strategies ⋮ The Matita Interactive Theorem Prover ⋮ Whelp ⋮ Experiences from exporting major proof assistant libraries ⋮ Web Interfaces for Proof Assistants

Uses Software

• Unnamed Item
• C-CoRN
• MML

This page was built for publication: Types for Proofs and Programs