Elf

swMATH21361MaRDI QIDQ33169FDOQ33169

Author name not available (Why is that?)

Official website: https://www.cs.cmu.edu/~fp/elf.html

Cited In (72)

• 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
• Higher-order pattern complement and the strict \(\lambda\)-calculus
• A natural deduction approach to dynamic logic
• Lolli
• 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
• Title not available (Why is that?)
• A linear logical framework
• HiLog
• 2OBJ
• Automath
• Efficient resource management for linear logic proof search
• ALF
• PAGODA
• LEGO
• K-Maude
• DDebugger
• CARIBOO
• vlogsl
• Pesca
• Programming inductive proofs. A new approach based on contextual types
• K-Java
• KJS
• CafeInMaude
• KANREN
• SPEC
• SymPLFIED
• TIL
• CITP
• SKIL
• Light-weight Containers
• MiniML
• PRIZ
• Cambridge LCF
• Title not available (Why is that?)
• Logical frameworks
• Representing proof transformations for program optimization
• Metamath Zero
• 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
• Programming type-safe transformations using higher-order abstract syntax
• Proof-search in type-theoretic languages: An introduction
• Using typed lambda calculus to implement formal systems on a machine
• A Maude environment for CafeOBJ
• Title not available (Why is that?)
• Program development schemata as derived rules
• The practice of logical frameworks

This page was built for software: Elf