Elf
From MaRDI portal
Software:33169
No author found.
Related Items (46)
Structured theory presentations and logic representations ⋮ Linear unification of higher-order patterns ⋮ A note on the proof theory of the \(\lambda \Pi\)-calculus ⋮ Higher-order superposition for dependent types ⋮ Verifying termination and reduction properties about higher-order logic programs ⋮ A modal analysis of staged computation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Programming Type-Safe Transformations Using Higher-Order Abstract Syntax ⋮ A notation for lambda terms. A generalization of environments ⋮ Twenty years of rewriting logic ⋮ A linear logical framework ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Forum: A multiple-conclusion specification logic ⋮ A natural deduction approach to dynamic logic ⋮ Unnamed Item ⋮ A Maude environment for CafeOBJ ⋮ Using typed lambda calculus to implement formal systems on a machine ⋮ Unification under a mixed prefix ⋮ A Graph-Theoretic Approach to Sequent Derivability in the Lambek Calculus ⋮ Unnamed Item ⋮ A module system for a programming language based on the LF logical framework ⋮ A framework for proof systems ⋮ Unnamed Item ⋮ Programming Inductive Proofs ⋮ Primitive recursion for higher-order abstract syntax ⋮ Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation ⋮ Representing proof transformations for program optimization ⋮ Decidable higher-order unification problems ⋮ Elf: A meta-language for deductive systems ⋮ A Linear Spine Calculus ⋮ Isabelle's metalogic: formalization and proof checker ⋮ Unification with extended patterns ⋮ Mechanized metatheory revisited ⋮ Efficient resource management for linear logic proof search ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Program development schemata as derived rules ⋮ Mathematical Knowledge Management ⋮ Automated techniques for provably safe mobile code. ⋮ Structural cut elimination. I: Intuitionistic and classical logic ⋮ Implementing tactics and tacticals in a higher-order logic programming language ⋮ A formalization and proof checker for Isabelle's metalogic ⋮ Higher-order pattern complement and the strict λ-calculus ⋮ The practice of logical frameworks
This page was built for software: Elf
