Sciweavers

SLOGICA
1998
128views more  SLOGICA 1998»
14 years 3 days ago
Encoding Modal Logics in Logical Frameworks
We present and discuss various formalizations of Modal Logics in Logical Frameworks based on Type Theories. We consider both Hilbert- and Natural Deductionstyle proof systems for ...
Arnon Avron, Furio Honsell, Marino Miculan, Cristi...
ENTCS
2007
95views more  ENTCS 2007»
14 years 12 days ago
Hybridizing a Logical Framework
Logical connectives familiar from the study of hybrid logic can be added to the logical framework LF, a constructive type theory of dependent functions. This extension turns out t...
Jason Reed
ENTCS
2007
113views more  ENTCS 2007»
14 years 12 days ago
A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F
We formalize in the logical framework ATS/LF a proof based on Tait’s method that establishes the simply-typed lambda-calculus being strongly normalizing. In malization, we emplo...
Kevin Donnelly, Hongwei Xi
ENTCS
2008
99views more  ENTCS 2008»
14 years 15 days ago
Specifying Properties of Concurrent Computations in CLF
CLF (the Concurrent Logical Framework) is a language for specifying and reasoning about concurrent systems. Its most significant feature is the first-class representation of concu...
Kevin Watkins, Iliano Cervesato, Frank Pfenning, D...
ENTCS
2008
101views more  ENTCS 2008»
14 years 15 days ago
Imperative LF Meta-Programming
Logical frameworks have enjoyed wide adoption as meta-languages for describing deductive systems. While the techniques for representing object languages in logical frameworks are ...
Aaron Stump