Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
90 | Matthias M. Hölzl, John N. Crossley |
Disjunctive Constraint Lambda Calculi. |
LPAR |
2005 |
DBLP DOI BibTeX RDF |
|
88 | Bart Jacobs 0001 |
Semantics of lambda-I and of other substructure lambda calculi. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
84 | Luigi Liquori |
Type Assigment Systems for Lambda Calculi and for the Lambda Calculus of Objects. (Sistemi di Assegnamento di tipi per il lambda calcolo e per il lambda calcolo degli oggetti / Systèmes d'inférence de type pour le lambda-calcul et pour le lambda-calcul à objets). |
|
1996 |
RDF |
|
81 | Stefan Blom |
An Approximation Based Approach to Infinitary Lambda Calculi. |
RTA |
2004 |
DBLP DOI BibTeX RDF |
infinitary rewriting, lambda calculus |
80 | Yohji Akama |
Limiting Partial Combinatory Algebras towards Infinitary Lambda-Calculi and Classical Logic. |
CSL |
2001 |
DBLP DOI BibTeX RDF |
partial combinatory algebra, limiting recursive functions, realizability interpretation, infinitary lambda-calculi, In the interpretation, ?-variables(=continuations) are interpreted as streams of -terms, calculus, discontinuity |
76 | Masahito Hasegawa |
Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculi. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
76 | Marina Lenisa |
Semantic Techniques for Deriving Coinductive Characterizations of Observational Equivalences for Lambda-calculi. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
76 | Pawel Urzyczyn |
Inhabitation in Typed Lambda-Calculi (A Syntactic Approach). |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
76 | Hongwei Xi |
Weak and Strong Beta Normalisations in Typed Lambda-Calculi. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
76 | Paul-André Melliès |
Typed lambda-calculi with explicit substitutions may not terminate. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
76 | Masako Takahashi |
Lambda-Calculi with Conditional Rules. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
73 | Matthias M. Hölzl, John N. Crossley |
Constraint-Lambda Calculi. |
FroCoS |
2002 |
DBLP DOI BibTeX RDF |
|
65 | Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano |
Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence. |
CSL |
2008 |
DBLP DOI BibTeX RDF |
domain-free type system, undecidability, existential type, CPS-translation |
65 | José Espírito Santo |
Delayed Substitutions. |
RTA |
2007 |
DBLP DOI BibTeX RDF |
|
65 | Manfred Schmidt-Schauß |
Correctness of Copy in Calculi with Letrec. |
RTA |
2007 |
DBLP DOI BibTeX RDF |
|
65 | Jean Goubault-Larrecq, Slawomir Lasota 0001, David Nowak, Yu Zhang |
Complete Lax Logical Relations for Cryptographic Lambda-Calculi. |
CSL |
2004 |
DBLP DOI BibTeX RDF |
Cryptographic lambda-calculus, Subscone, Monads, Logical relations |
62 | Yu Zhang, David Nowak |
Logical Relations for Dynamic Name Creation. |
CSL |
2003 |
DBLP DOI BibTeX RDF |
Kripke logical relation, name creation, nu-calculus, categorical models of lambda calculi |
57 | Flemming Nielson, Hanne Riis Nielson |
Prescriptive Frameworks for Multi-Level Lambda-Calculi. |
PEPM |
1997 |
DBLP DOI BibTeX RDF |
|
56 | Davide Sangiorgi, Naoki Kobayashi 0001, Eijiro Sumii |
Environmental Bisimulations for Higher-Order Languages. |
LICS |
2007 |
DBLP DOI BibTeX RDF |
|
55 | Slawomir Lasota 0001, David Nowak, Yu Zhang |
On Completeness of Logical Relations for Monadic Types. |
ASIAN |
2006 |
DBLP DOI BibTeX RDF |
|
51 | Philippe de Groote (eds.) |
Typed Lambda Calculi and Applications, Third International Conference on Typed Lambda Calculi and Applications, TLCA '97, Nancy, France, April 2-4, 1997, Proceedings |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Ferruccio Damiani, Paola Giannini |
An Inference Algorithm for Strictness. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Harald Rueß |
Computational Reflection in the Calculus of Constructions and its Application to Theorem Proving. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Toshihiko Kurata |
A Type Theoretical View of Böhm-Trees. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Judicaël Courant |
A Module Calculus for Pure Type Systems. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Ian Stark |
Names, Equations, Relations: Practical Ways to Reason about new. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Hugo Herbelin |
Games and Weak-Head Reduction for Classical PCF. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Izumi Takeuti |
An Axiomatic System of Parametricity. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Torben Braüner |
A Simple Adequate Categorical Model for PCF. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Stefano Berardi, Luca Boerio |
Minimum Information Code in a Pure Functional Language with Data Types. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Antonio Bucciarelli |
Logical Reconstruction of Bi-domains. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Christian Retoré |
Pomset Logic: A Non-commutative Extension of Classical Linear Logic. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Femke van Raamsdonk |
Outermost-Fair Rewriting. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Joëlle Despeyroux, Frank Pfenning, Carsten Schürmann |
Primitive Recursion for Higher-Order Abstract Syntax. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Stefano Guerrini, Simone Martini 0001, Andrea Masini |
Proof Nets, Garbage, and Computations. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Michael Brandt, Fritz Henglein |
Coinductive Axiomatization of Recursive Type Equality and Subtyping. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Viviana Bono, Michele Bugliesi |
Matching Constraints for the Lambda Calculus of Objects. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Yohji Akama |
A Lambda-to-CL Translation for Strong Normalization. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Jan Malolepszy, Malgorzata Moczurad, Marek Zaionc |
Schwichtenberg-Style Lambda Definability Is Undecidable. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Gianna Bellè, Eugenio Moggi |
Typed Intermediate Languages for Shape Analysis. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Neil Ghani |
Eta-Expansions in Dependent Type Theory - The Calculus of Constructions. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
51 | Mariangiola Dezani-Ciancaglini, Gordon D. Plotkin (eds.) |
Typed Lambda Calculi and Applications, Second International Conference on Typed Lambda Calculi and Applications, TLCA '95, Edinburgh, UK, April 10-12, 1995, Proceedings |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | M. Randall Holmes |
Untyped lambda-Calculus with Relative Typing. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Vincent Padovani |
On Equivalence Classes of Interpolation Equations. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Alberto Pravato, Simona Ronchi Della Rocca, Luca Roversi |
Categorical semantics of the call-by-value lambda-calculus. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Antonius J. C. Hurkens |
A Simplification of Girard's Paradox. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Roberto Bellucci, Martín Abadi, Pierre-Louis Curien |
A Model for Formal Parametric Polymorphism: A PER Interpretation for System R. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Healfdene Goguen |
Typed Operational Semantics. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Neil Ghani |
ßn-Equality for Coproducts. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Yann Coscoy, Gilles Kahn, Laurent Théry |
Extracting Text from Proofs. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Toshihiko Kurata, Masako Takahashi |
Decidable Properties of Intersection Type Systems. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Gavin M. Bierman |
What is a Categorical Model of Intuitionistic Linear Logic? |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Gilles Barthe |
Extensions of Pure Type Systems. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | François Leclerc |
Termination Proof of Term Rewriting System with the Multiset Path Ordering. A Complete Development in the System Coq. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Furio Honsell, Marina Lenisa |
Final Semantics for untyped lambda-calculus. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Roberto Di Cosmo, Adolfo Piperno |
Expanding Extensional Polymorphism. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Eike Ritter, Andrew M. Pitts |
A Fully Abstract Translation between a Lambda-Calculus with Reference Types and Standard ML. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Robert Pollack |
A Verified Typechecker. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Stefano Berardi, Marc Bezem, Thierry Coquand |
A realization of the negative interpretation of the Axiom of Choice. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Hidetaka Kondoh |
Basic Properties of Data Types with Inequational Refinements. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Jan Springintveld |
Third-Order Matching in the Presence of Type Constructors. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Gilles Dowek |
Lambda-calculus, Combinators and the Comprehension Scheme. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Stefano Berardi, Luca Boerio |
Using Subtyping in Program Optimization. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Alex K. Simpson |
Categorical completeness results for the simply-typed lambda-calculus. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Joëlle Despeyroux, Amy P. Felty, André Hirschowitz |
Higher-Order Abstract Syntax in Coq. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Jaco van de Pol, Helmut Schwichtenberg |
Strict Functionals for Termination Proofs. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Philippe de Groote |
A Simple Calculus of Exception Handling. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Daniel Briaud |
An explicit Eta rewrite rule. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Martin Hofmann 0001 |
A Simple Model for Quotient Types. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Andrea Asperti, Cosimo Laneve |
Comparing Lambda-calculus translations in Sharing Graphs. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
51 | Marc Bezem, Jan Friso Groote (eds.) |
Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Hans Leiß |
Combining Recursive and Dynamic Types. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Jan Springintveld |
Lower and Upper Bounds for Reductions of Types in Lambda-omega and Lambda-P. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Pietro Di Gianantonio, Furio Honsell |
An Abstract Notion of Application. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | J. M. E. Hyland, C.-H. Luke Ong |
Modified Realizability Toposes and Strong Normalization Proofs. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Tobias Nipkow |
Orthogonal Higher-Order Rewrite Systems are Confluent. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Gilles Dowek |
The Undecidability of Typability in the Lambda-Pi-Calculus. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Franco Barbanera, Stefano Berardi |
Extracting Constructive Content from Classical Logic via Control-like Reductions. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Giorgio Ghelli |
Recursive Types Are not Conservative over F. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Benjamin C. Pierce |
Intersection Types and Bounded Polymorphism. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Kurt Sieber |
Call-by-Value and Nondeterminism. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | James McKinna, Robert Pollack |
Pure Type Systems Formalized. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Philippe de Groote |
The Conservation Theorem revisited. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Pawel Urzyczyn |
Type reconstruction in F-omega is undecidable. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Daniel Leivant, Jean-Yves Marion |
Lambda calculus characterizations of poly-time. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Franco Barbanera, Maribel Fernández |
Combining First and Higher Order Rewrite Systems with Type Assignment Systems. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Christine Paulin-Mohring |
Inductive Definitions in the system Coq - Rules and Properties. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Giuseppe Castagna, Giorgio Ghelli, Giuseppe Longo |
A Semantics for Lambda&-early: A Calculus with Overloading and Early Binding. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Achim Jung, Jerzy Tiuryn |
A New Characterization of Lambda Definability. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Bart Jacobs 0001, Thomas F. Melham |
Translating Dependent Type Theory into Higher Order Logic. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Achim Jung, Allen Stoughton |
Studying the Fully Abstract Model of PCF within its Continuous Function Model. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Ulrich Berger 0001 |
Program Extraction from Normalization Proofs. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Yohji Akama |
On Mints' Reduction for ccc-Calculus. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Daniel F. Otth |
Monotonic versus Antimonotonic Exponentation. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | P. N. Benton, Gavin M. Bierman, Valeria de Paiva, Martin Hyland |
A Term Calculus for Intuitionistic Linear Logic. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Thorsten Altenkirch |
A Formalization of the Strong Normalization Proof for System F in LEGO. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Gordon D. Plotkin, Martín Abadi |
A Logic for Parametric Polymorphism. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
51 | Steffen van Bakel |
Partial Intersection Type Assignment in Applicative Term Rewriting Systems. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
49 | Marcelo P. Fiore, Roberto Di Cosmo, Vincent Balat |
Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types. |
LICS |
2002 |
DBLP DOI BibTeX RDF |
|
49 | Peter W. O'Hearn |
Resource Interpretations, Bunched Implications and the alpha lambda-Calculus. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|