scientific article; zbMATH DE number 2085175

zbMath1054.03501MaRDI QIDQ4736399

Conor McBride

Publication date: 9 August 2004

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

interactive proofelimination rules

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Supercompilation for Martin-Lof's type theory, Cubical methods in homotopy type theory and univalent foundations, From realizability to induction via dependent intersection, Trace-Based Coinductive Operational Semantics for While, A Reflection on Types, Strongly typed term representations in Coq, Foundations of dependent interoperability, Quotients by Idempotent Functions in Cedille, Propositional forms of judgemental interpretations, Formally proving size optimality of sorting networks, Formal metatheory of programming languages in the Matita interactive theorem prover, Eliminating dependent pattern matching without K, Mac Lane's comparison theorem for the Kleisli construction formalized in Coq, Congruence Closure in Intensional Type Theory

Uses Software

• Coq
• LEGO