Results 1 to 10 of about 48 (45)
COMBINATORY LOGIC AND $ lambda $-CALCULUS FOR CLASSICAL LOGIC [PDF]
Bulletin of Informatics and Cybernetics, 2000 Summary: Since Griffin's work in 1990, classical logic has been an attractive target for extracting computational contents. However, the classical principle used in Griffin's type system is the double-negation-elimination rule, which prevents one to analyze the intuitionistic part and the purely classical part separately. By formulating a calculus with
Sachio Hirokawa, Kensuke Baba
exaly +3 more sources
Binary Lambda Calculus and Combinatory Logic [PDF]
, 2007 We introduce binary representations of both lambda calculus and combinatory logic terms, and demonstrate their simplicity by providing very compact parser-interpreters for these binary languages. We demonstrate their application to Algorithmic Information Theory with several concrete upper bounds on program-size complexity, including an elegant ...
exaly +5 more sources
Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic
Logical Methods in Computer ScienceA system $\boldsymbolλ_θ$ is developed that combines modal logic and simply-typed lambda calculus, and that generalizes the system studied by Montague and Gallin. Whereas Montague and Gallin worked with Church's simple theory of types, the system $\boldsymbolλ_θ$ is developed in the typed base theory most commonly used today, namely the simply-typed ...
exaly +3 more sources
Addressing Machines as models of lambda-calculus [PDF]
Logical Methods in Computer Science, 2022 Turing machines and register machines have been used for decades in theoretical computer science as abstract models of computation. Also the $\lambda$-calculus has played a central role in this domain as it allows to focus on the notion of functional ...
Giuseppe Della Penna +2 more
doaj +1 more source
Asymptotically almost all \lambda-terms are strongly normalizing [PDF]
Logical Methods in Computer Science, 2013 We present quantitative analysis of various (syntactic and behavioral) properties of random \lambda-terms. Our main results are that asymptotically all the terms are strongly normalizing and that any fixed closed term almost never appears in a random ...
René David +5 more
doaj +1 more source
Encoding the Factorisation Calculus [PDF]
Electronic Proceedings in Theoretical Computer Science, 2015 Jay and Given-Wilson have recently introduced the Factorisation (or SF-) calculus as a minimal fundamental model of intensional computation. It is a combinatory calculus containing a special combinator, F, which is able to examine the internal structure ...
Reuben N. S. Rowe
doaj +1 more source
RPO, Second-order Contexts, and Lambda-calculus [PDF]
Logical Methods in Computer Science, 2009 First, we extend Leifer-Milner RPO theory, by giving general conditions to obtain IPO labelled transition systems (and bisimilarities) with a reduced set of transitions, and possibly finitely branching.
Pietro Di Gianantonio +2 more
doaj +1 more source
Mixin Composition Synthesis based on Intersection Types [PDF]
Logical Methods in Computer Science, 2018 We present a method for synthesizing compositions of mixins using type inhabitation in intersection types. First, recursively defined classes and mixins, which are functions over classes, are expressed as terms in a lambda calculus with records ...
Jan Bessai +5 more
doaj +1 more source
Combinatory Logic and Lambda Calculus Are Equal, Algebraically.
, 2023 It is well-known that extensional lambda calculus is equivalent to extensional combinatory logic. In this paper we describe a formalisation of this fact in Cubical Agda. The distinguishing features of our formalisation are the following: (i) Both languages are defined as generalised algebraic theories, the syntaxes are intrinsically typed and ...
Altenkirch, Thorsten +3 more
openaire +3 more sources
A correct-by-construction conversion from lambda calculus to combinatory logic
Journal of Functional Programming, 2023 Abstract This pearl defines a translation from well-typed lambda terms to combinatory logic, where both the preservation of types and the correctness of the translation are enforced statically.
openaire +3 more sources