Elf

swMATH21361MaRDI QIDQ33169FDOQ33169

Author name not available (Why is that?)

Cited In (46)

• Automated techniques for provably safe mobile code.
• Twenty years of rewriting logic
• Structural cut elimination. I: Intuitionistic and classical logic
• A framework for proof systems
• A Linear Spine Calculus
• Mechanized metatheory revisited
• Extending the TPTP Language to Higher-Order Logic with Automated Parser Generation
• A graph-theoretic approach to sequent derivability in the Lambek calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Unification with extended patterns
• A natural deduction approach to dynamic logic
• Title not available (Why is that?)
• Forum: A multiple-conclusion specification logic
• A notation for lambda terms. A generalization of environments
• Primitive recursion for higher-order abstract syntax
• Linear unification of higher-order patterns
• Verifying termination and reduction properties about higher-order logic programs
• A module system for a programming language based on the LF logical framework
• Programming Type-Safe Transformations Using Higher-Order Abstract Syntax
• Title not available (Why is that?)
• A linear logical framework
• Efficient resource management for linear logic proof search
• Programming inductive proofs. A new approach based on contextual types
• Title not available (Why is that?)
• Logical frameworks
• Representing proof transformations for program optimization
• Mathematical Knowledge Management
• Isabelle's metalogic: formalization and proof checker
• A formalization and proof checker for Isabelle's metalogic
• Decidable higher-order unification problems
• A note on the proof theory of the \(\lambda \Pi\)-calculus
• Implementing tactics and tacticals in a higher-order logic programming language
• Unification under a mixed prefix
• Higher-order superposition for dependent types
• A modal analysis of staged computation
• Title not available (Why is that?)
• Elf: A meta-language for deductive systems
• Structured theory presentations and logic representations
• Proof-search in type-theoretic languages: An introduction
• Using typed lambda calculus to implement formal systems on a machine
• A Maude environment for CafeOBJ
• Higher-order pattern complement and the strict λ-calculus
• Title not available (Why is that?)
• Program development schemata as derived rules
• The practice of logical frameworks

This page was built for software: Elf