A Modular Type Reconstruction Algorithm

DOI10.1145/3234693zbMath1407.68440OpenAlexW2903910822WikidataQ128703535 ScholiaQ128703535MaRDI QIDQ4617969

Florian Rabe

Publication date: 7 February 2019

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3234693

zbMATH Keywords

modularitylogical frameworkdependent typestype reconstructionMmt

Mathematics Subject Classification ID

Related Items (4)

Equality Checking for General Type Theories in Andromeda 2 ⋮ Making PVS accessible to generic services by interpretation in a universal format ⋮ An extensible equality checking algorithm for dependent type theories ⋮ Logic-independent proof search in logical frameworks (short paper)

Uses Software

• Coq
• Isabelle
• Beluga
• PVS
• Isar
• MMT
• Abella
• Agda
• HOLyHammer
• LATIN
• LLFp
• Delphin
• ELPI

This page was built for publication: A Modular Type Reconstruction Algorithm