Elf
The Elf Meta-Language. Elf is a constraint logic programming language based on the LF Logical Framework. It has no connection whatsoever to the ELF® statistical package, a commercial product by The Winchendon Group, Inc. Elf is a uniform meta-language for specifying, implementing, and proving properties of programming languages and logics. It has been applied to various examples, some of which are described in published papers accessible through a bibliography on LF and Elf. Others are described in the notes to a course on Computation and Deduction, which are not yet publicly available. There is also a more complete bibliography on logical frameworks in general. Work on LF and Elf at Carnegie Mellon University is supported by NSF grant CCR-9303383 (Principal Investigators Robert Harper and Frank Pfenning)
Keywords for this software
References in zbMATH (referenced in 44 articles , 2 standard articles )
Showing results 1 to 20 of 44.
Sorted by year (- Nipkow, Tobias; Roßkopf, Simon: Isabelle’s metalogic: formalization and proof checker (2021)
- Miller, Dale: Mechanized metatheory revisited (2019)
- Riesco, Adrián; Ogata, Kazuhiro; Futatsugi, Kokichi: A Maude environment for CafeOBJ (2017)
- Savary-Belanger, Olivier; Monnier, Stefan; Pientka, Brigitte: Programming type-safe transformations using higher-order abstract syntax (2013)
- Meseguer, José: Twenty years of rewriting logic (2012)
- Nigam, Vivek; Miller, Dale: A framework for proof systems (2010)
- Pientka, Brigitte: Programming inductive proofs. A new approach based on contextual types (2010)
- Van Gelder, Allen; Sutcliffe, Geoff: Extending the TPTP language to higher-order logic with automated parser generation (2006)
- Pientka, Brigitte: Verifying termination and reduction properties about higher-order logic programs (2005)
- Kutsia, Temur; Buchberger, Bruno: Predicate logic with sequence variables and sequence function symbols (2004)
- Penn, Gerald: A graph-theoretic approach to sequent derivability in the Lambek calculus (2004)
- Cervesato, Iliano; Pfenning, Frank: A linear spine calculus (2003)
- Colby, Christopher; Crary, Karl; Harper, Robert; Lee, Peter; Pfenning, Frank: Automated techniques for provably safe mobile code. (2003)
- Momigliano, Alberto; Pfenning, Frank: Higher-order pattern complement and the strict (\lambda)-calculus (2003)
- Cervesato, Iliano; Pfenning, Frank: A linear logical framework (2002)
- Pfenning, Frank: Logical frameworks -- a brief introduction (2002)
- Davies, Rowan; Pfenning, Frank: A modal analysis of staged computation (2001)
- Pfenning, Frank: Logical frameworks (2001)
- Schürmann, C.; Despeyroux, J.; Pfenning, F.: Primitive recursion for higher-order abstract syntax (2001)
- Anderson, Penny; Basin, David: Program development schemata as derived rules (2000)