A5081098905- Logic, programming, and type systems
- Logic, Reasoning, and Knowledge
- Formal Methods in Verification
- Computability, Logic, AI Algorithms
- Advanced Algebra and Logic
- semigroups and automata theory
- Semantic Web and Ontologies
- Multi-Agent Systems and Negotiation
- Model-Driven Software Engineering Techniques
- Parallel Computing and Optimization Techniques
- Internet Traffic Analysis and Secure E-voting
- Natural Language Processing Techniques
- Spam and Phishing Detection
- Matrix Theory and Algorithms
- Geometric and Algebraic Topology
- Hate Speech and Cyberbullying Detection
- Advanced Database Systems and Queries
- Homotopy and Cohomology in Algebraic Topology
- Advanced Topology and Set Theory
- Software Engineering Research
- Complexity and Algorithms in Graphs
- Cognitive Science and Mapping
- Machine Learning and Algorithms
- Mathematics, Computing, and Information Processing
- Advanced Combinatorial Mathematics
University of Warsaw
2012-2024
Institute of Mathematics
1983-2006
Institute of Informatics of the Slovak Academy of Sciences
1989-2005
University of Warmia and Mazury in Olsztyn
1983-2003
Cornell University
1994
Fondation Sophia Antipolis
1994
University of Edinburgh
1994
Boston University
1993
Institute of Mathematics and Informatics
1990
Czech Academy of Sciences, Institute of Mathematics
1982-1990
article Free AccessType reconstruction in the presence of polymorphic recursion Authors: A. J. Kfoury Boston University UniversityView Profile , Tiuryn Warsaw WarsawView P. Urzyczyn Authors Info & Claims ACM Transactions on Programming Languages and SystemsVolume 15Issue 2pp 290–311https://doi.org/10.1145/169701.169687Published:01 April 1993Publication History 50citation541DownloadsMetricsTotal Citations50Total Downloads541Last 12 Months46Last 6 weeks5 Get Citation AlertsNew Alert added!This...
We carry out an analysis of typability terms in ML. Our main result is that this problem DEXPTIME-hard, where by DEXPTIME we mean DTIME(2 n 0(1) ). This, together with the known exponential-time algorithm solves problem, yields DEXPTIME-completeness result. This settles open P. Kanellakis and J. C. Mitchell. Part our algebraic characterization ML a restricted form semi-unification, which identify as acyclic semi-unification . prove can be reduced to each other polynomial time. believe...
Article Free AccessThe undecidability of the semi-unification problem Authors: A. J. Kfoury Dept Computer Science, Boston University UniversityView Profile , Tiuryn Institute Mathematics, Warsaw WarsawView P. Urzyczyn Authors Info & Claims STOC '90: Proceedings twenty-second annual ACM symposium on Theory ComputingApril 1990 Pages 468–476https://doi.org/10.1145/100216.100279Published:01 April 1990Publication History 23citation433DownloadsMetricsTotal Citations23Total Downloads433Last 12...
Abstract We study the intersection type assignment system as defined by Barendregt, Coppo and Dezani. For four essential variants of (with without a universal with subtyping) we show that emptiness (inhabitation) problem is recursively unsolvable. That is, there no effective algorithm to decide if closed term given type. It follows provability in logic “strong conjunction” Mints Lopez-Escobar also undecidable.
In combinatory logic one usually assumes a fixed set of basic combinators (axiom schemes), K and S. this setting the provable formulas (inhabited types) is PSPACE-complete in simple types undecidable intersection types. When arbitrary sets axiom schemes are considered, inhabitation problem even (this known as Linial-Post theorem). k-bounded with arises from by imposing bound k on depth (formulae) which may be substituted for type variables schemes. We consider (provability) k-bounded...
Positive recursive (fixpoint) types can be added to the polymorphic (Church-style) lambda calculus λ2 (System F) in several different ways, depending on choice of elimination operator. We compare such definitions and we show that they fall into two equivalence classes with respect mutual interpretability by means beta-eta reductions. Elimination operators for fixpoint are thus classified as either iterators or recursors. This classification has an interpretation terms Curry-Howard...
A generalization of first-order unification, called semiunification, is studied with two goals in mind: (1) type-checking functional programs relative to an improved polymorphic type discipline; and (2) deciding the typability terms a restricted form lambda -calculus.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>
We extend the functional language ML by allowing recursive calls to a function F on right-hand side of its definition be at different types, all generic instances (derived) type left-hand definition. The original does not allow this feature. This extension produce new types beyond usual universal polymorphic and satisfies properties already enjoyed ML: principal-type property effective type-assignment property.
We prove that the subtyping problem induced by Mitchell's containment relation (1988) for second-order polymorphic types is undecidable. It follows type-checking undecidable lambda-calculus extended an appropriate subsumption rule.
The provability problem in intuitionistic propositional second-order logic with existential quantifier and implication (∃,→) is proved to be undecidable presence of free type variables (constants). This contrasts the result that inutitionistic quantifier, conjunction negation decidable.