Formal metatheory of programming languages in the Matita interactive theorem prover
From MaRDI portal
Publication:1945919
DOI10.1007/s10817-011-9228-zzbMath1260.68363OpenAlexW1982618236WikidataQ126277594 ScholiaQ126277594MaRDI QIDQ1945919
Wilmer Ricciotti, Enrico Tassi, Claudio Sacerdoti Coen, Andrea Asperti
Publication date: 17 April 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-011-9228-z
Uses Software
Cites Work
- Unnamed Item
- A compact kernel for the calculus of inductive constructions
- An extension of system \(F\) with subtyping
- Nominal logic, a first order theory of names and binding
- User interaction with the Matita proof assistant
- Tinycals: Step by Step Tacticals
- Engineering formal metatheory
- Crafting a Proof Assistant
- Theorem Proving in Higher Order Logics