Cited in
(only showing first 100 items - show all)- Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
- Higher-order term indexing using substitution trees
- scientific article; zbMATH DE number 2036328 (Why is no real title available?)
- Intuitionistic completeness of first-order logic
- Programs using syntax with first-class binders
- Reasoning in Abella about structural operational semantics specifications
- Automated techniques for provably safe mobile code.
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- Intuitionistic Letcc via Labelled Deduction
- A logical framework combining model and proof theory
- The future of logic: foundation-independence
- Rensets and renaming-based recursion for syntax with bindings
- Theorem Proving in Higher Order Logics
- A scalable module system
- Structural focalization
- α lean TA P: A Declarative Theorem Prover for First-Order Classical Logic
- Building reliable, high-performance networks with the Nuprl proof development system
- scientific article; zbMATH DE number 1765685 (Why is no real title available?)
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- \textsc{Lincx}: a linear logical framework with first-class contexts
- A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- A Linear Spine Calculus
- Producing certified functional code from inductive specifications
- Representing model theory in a type-theoretical logical framework
- scientific article; zbMATH DE number 1231700 (Why is no real title available?)
- Proof search and proof check for equational and inductive theorems.
- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
- Contextual modal type theory
- scientific article; zbMATH DE number 2090533 (Why is no real title available?)
- Combining source, content, presentation, narration, and relational representation
- Termination checking with types
- Encoding functional relations in Scunak
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Canonical HybridLF: extending Hybrid with dependent types
- Mechanized metatheory revisited
- Formal logic definitions for interchange languages
- Functions-as-constructors higher-order unification: extended pattern unification
- Visible type application
- Automatically splitting a two-stage lambda calculus
- Automating theorem proving with SMT
- Efficient substitution in Hoare logic expressions
- A language-based approach to functionally correct imperative programming
- An improved proof-theoretic compilation of logic programs
- A framework for defining logical frameworks
- Higher-order dynamic pattern unification for dependent types and records
- The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
- Towards proof planning for \(\mathcal{M}_{\omega}^+\)
- scientific article; zbMATH DE number 1303348 (Why is no real title available?)
- A formal framework for specifying sequent calculus proof systems
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- Proof checking and logic programming
- In praise of impredicativity: a contribution to the formalization of meta-programming
- The Abella Interactive Theorem Prover (System Description)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
- Proof checking and logic programming
- First-Order Logic with Dependent Types
- Mechanizing metatheory in a logical framework
- Ruler: Programming Type Rules
- Choices in representation and reduction strategies for lambda terms in intensional contexts
- Towards MKM in the large: modular representation and scalable software architecture
- Towards logical frameworks in the heterogeneous tool set Hets
- Flexary operators for formalized mathematics
- Extending MKM formats at the statement level
- Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory
- Celf – A Logical Framework for Deductive and Concurrent Systems (System Description)
- Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism
- A formalized general theory of syntax with bindings: extended version
- Mechanizing metatheory without typing contexts
- Nominal abstraction
- Linearity Constraints as Bounded Intervals in Linear Logic Programming
- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
- Mechanizing the metatheory of LF
- Formalizing operational semantic specifications in logic
- Optimizing higher-order pattern unification.
- Verifying termination and reduction properties about higher-order logic programs
- Automated Deduction – CADE-19
- A case study in programming coinductive proofs: Howe's method
- General bindings and alpha-equivalence in Nominal Isabelle
- \(\mathrm{HO}\pi\) in Coq
- Logical relations for a logical framework
- Project abstract: logic atlas and integrator (LATIN)
- Generic literals
- The Mizar Mathematical Library in OMDoc: translation and applications
- N. G. de Bruijn's contribution to the formalization of mathematics
- Lax theory morphisms
- Implementing Cantor's paradise
- A canonical locally named representation of binding
- Verification, Model Checking, and Abstract Interpretation
- Dependent types ensure partial correctness of theorem provers
- Theorem Proving in Higher Order Logics
- Coq
- HYBRID
- ILTP
- Isabelle
- Ott
- TALP
- ML
- TPS
- Beluga
This page was built for software: Twelf
