scientific article
From MaRDI portal
Publication:2751369
zbMath0992.03038MaRDI QIDQ2751369
Publication date: 27 August 2002
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
natural deductionlogical frameworkproof searchmeta-programmingabstract syntaxjudgmentshereditary Harrop formulasLF type theoryspecification of deductive systems
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Formal Logic Definitions for Interchange Languages, Directly reflective meta-programming, Encoding abstract syntax without fresh names, Formalizing adequacy: a case study for higher-order abstract syntax, Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics, Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge, Finitary type theories with and without contexts, A linear logical framework, Cut elimination for a logic with induction and co-induction, A complete uniform substitution calculus for differential dynamic logic, Decidability of bounded higher-order unification, Efficient Substitution in Hoare Logic Expressions, A Third-Order Representation of the λμ-Calculus, Flexary Operators for Formalized Mathematics, Automated techniques for provably safe mobile code., On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions, A Framework for Defining Logical Frameworks, Normalization for the Simply-Typed Lambda-Calculus in Twelf, Imperative LF Meta-Programming, The future of logic: foundation-independence
Uses Software
