[图书][B] A modern perspective on type theory: from its origins until today
FD Kamareddine, T Laan, R Nederpelt - 2004 - books.google.com
Towards the end of the nineteenth century, Frege gave us the abstraction principles and the
general notion of functions. Self-application of functions was at the heart of Russell's …
general notion of functions. Self-application of functions was at the heart of Russell's …
The Permutative λ-Calculus
B Accattoli, D Kesner - International Conference on Logic for Programming …, 2012 - Springer
We introduce the permutative λ-calculus, an extension of λ-calculus with three equations
and one reduction rule for permuting constructors, generalising many calculi in the literature …
and one reduction rule for permuting constructors, generalising many calculi in the literature …
Preservation of strong normalisation modulo permutations for the structural lambda-calculus
B Accattoli, D Kesner - Logical Methods in Computer Science, 2012 - lmcs.episciences.org
Inspired by a recent graphical formalism for lambda-calculus based on linear logic
technology, we introduce an untyped structural lambda-calculus, called lambda j, which …
technology, we introduce an untyped structural lambda-calculus, called lambda j, which …
Enfragmo: A system for modelling and solving search problems with logic
In this paper, we present the Enfragmo system for specifying and solving combinatorial
search problems. It supports natural specification of problems by providing users with a rich …
search problems. It supports natural specification of problems by providing users with a rich …
On strong normalization in the intersection type discipline
G Boudol - International Conference on Typed Lambda Calculi …, 2003 - Springer
We give a proof for the strong normalization result in the intersection type discipline, which
we obtain by putting together some well-known results and proof techniques. Our proof uses …
we obtain by putting together some well-known results and proof techniques. Our proof uses …
Normalisation is Insensible to\lambda-Term Identity or Difference
M Tatsuta, M Dezani-Ciancaglini - 21st Annual IEEE …, 2006 - ieeexplore.ieee.org
This paper analyses the computational behaviour of lambda-term applications. The
properties we are interested in are weak normalisation (ie there is a terminating reduction) …
properties we are interested in are weak normalisation (ie there is a terminating reduction) …
De bruijn's automath and pure type systems
F Kamareddine, T Laan, R Nederpelt - Thirty five years of automating …, 2003 - Springer
We study the position of the AUTOMATH systems within the framework of Pure Type
Systems (PTSs). In [Barendregt, 1992; Geuvers, 1993], a rough relationship has been given …
Systems (PTSs). In [Barendregt, 1992; Geuvers, 1993], a rough relationship has been given …
On the longest perpetual reductions in orthogonal expression reduction systems
Z Khasidashvili - Theoretical computer science, 2001 - Elsevier
We study perpetual reductions in orthogonal (or conflict-free) fully extended expression
reduction systems (OERS). ERS is a formalism for rewriting that subsumes term rewriting …
reduction systems (OERS). ERS is a formalism for rewriting that subsumes term rewriting …
On strong normalization and type inference in the intersection type discipline
G Boudol - Theoretical computer science, 2008 - Elsevier
We introduce a new unification procedure for the type inference problem in the intersection
type discipline. It is well known that type inference in this case should succeed exactly for the …
type discipline. It is well known that type inference in this case should succeed exactly for the …
[PDF][PDF] A short proof that adding some permutation rules to preserves
R David - arXiv preprint arXiv:1011.1335, 2010 - arxiv.org
arXiv:1011.1335v1 [cs.LO] 5 Nov 2010 Page 1 arXiv:1011.1335v1 [cs.LO] 5 Nov 2010 A short
proof that adding some permutation rules to β preserves SN René David LAMA - Equipe …
proof that adding some permutation rules to β preserves SN René David LAMA - Equipe …