Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Martin Berger 0001, Kohei Honda 0001, Nobuko Yoshida |
Sequentiality and the pi-Calculus. |
TLCA |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Paolo Coppola 0001, Simone Martini 0001 |
Typing Lambda Terms in Elementary Logic with Linear Constraints. |
TLCA |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Andrzej S. Murawski, C.-H. Luke Ong |
Evolving Games and Essential Nets for Affine Polymorphism. |
TLCA |
2001 |
DBLP DOI BibTeX RDF |
Full Completeness, Polymorphism, Linear Logic, Game Semantics |
1 | Luca Cardelli, Andrew D. Gordon 0001 |
Logical Properties of Name Restriction. |
TLCA |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Jorge Sousa Pinto |
Parallel Implementation Models for the lambda-Calculus Using the Geometry of Interaction. |
TLCA |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Olivier Danvy |
Many Happy Returns. |
TLCA |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Thorsten Altenkirch, Thierry Coquand |
A Finitary Subsystem of the Polymorphic lambda-Calculus. |
TLCA |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Vincent Padovani |
Retracts in Simple Types. |
TLCA |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Healfdene Goguen |
Soundness of the Logical Framework for Its Typed Operational Semantics. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Atsushi Ohori |
A Curry-Howard Isomorphism for Compilation and Program Execution. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Peter Dybjer, Anton Setzer |
A Finite Axiomatization of Inductive-Recursive Definitions. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Christian Urban, Gavin M. Bierman |
Strong Normalisation of Cut-Elimination in Classical Logic. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Peter Harry Eidorff, Fritz Henglein, Christian Mossin, Henning Niss, Morten Heine Sørensen, Mads Tofte |
AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problem. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | V. Michele Abrusci |
Modules in Non-communicative Logic. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Peter W. O'Hearn |
Resource Interpretations, Bunched Implications and the alpha lambda-Calculus. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Masahiko Sato 0001, Takafumi Sakurai, Rod M. Burstall |
Explicit Environments. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Jan Zwanenburg |
Pure Type Systems with Subtyping. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Jeff Polakow, Frank Pfenning |
Natural Deduction for Intuitionistic Non-communicative Linear Logic. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Patrick Baillot, Marco Pedicini |
Elementary Complexity and Geometry of Interaction. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Ken-etsu Fujita |
Explicitly Typed lambda µ-Calculus for Polymorphism an Call-by-Value. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Olivier Laurent 0001 |
Polarized Proof-Nets: Proof-Nets for LC. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Nuno Barreiro, Thomas Ehrhard |
Quantitative Semantics Revisited. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Marcelo P. Fiore, Alex K. Simpson |
Lambda Definability with Sums via Grothendieck Logical Relations. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Jean-Marc Andreoli |
The Coordination Language Facility and Applications. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Eike Ritter |
Characterising Explicit Substitutions which Preserve Termination. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Stefano Berardi, Ugo de'Liguoro |
Total Functionals and Well-Founded Strategies. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | René David |
Every Unsolvable lambda Term has a Decoration. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Pietro Di Gianantonio, Gianluca Franco, Furio Honsell |
Game Semantics for Untyped lambda beta eta-Calculus. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Paul Blain Levy |
Call-by-Push-Value: A Subsuming Paradigm. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Richard Statman |
Consequences of Jacopini's Theorem: Consistent Equalities and Equations. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Sabine Broda, Luís Damas |
Counting a Type's Principal Inhabitants. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Seikoh Mikami, Yohji Akama |
A Study of Abramsky's Linear Chemical Abstract Machine. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Masahito Hasegawa |
Logical Predicates for Intuitionistic Linear Type Theories. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Erik Poll, Jan Zwanenburg |
A Logic for Abstract Data Types as Existential Types. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Ferruccio Damiani |
Useless-Code Detection and Elimination for PCF with Algebraic Data types. |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Jean-Yves Girard 0001 (eds.) |
Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings |
TLCA |
1999 |
DBLP DOI BibTeX RDF |
|
1 | Ferruccio Damiani, Paola Giannini |
An Inference Algorithm for Strictness. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Masahito Hasegawa |
Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculi. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Harald Rueß |
Computational Reflection in the Calculus of Constructions and its Application to Theorem Proving. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Marina Lenisa |
Semantic Techniques for Deriving Coinductive Characterizations of Observational Equivalences for Lambda-calculi. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Toshihiko Kurata |
A Type Theoretical View of Böhm-Trees. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Judicaël Courant |
A Module Calculus for Pure Type Systems. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Ian Stark |
Names, Equations, Relations: Practical Ways to Reason about new. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Hugo Herbelin |
Games and Weak-Head Reduction for Classical PCF. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Pawel Urzyczyn |
Inhabitation in Typed Lambda-Calculi (A Syntactic Approach). |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Izumi Takeuti |
An Axiomatic System of Parametricity. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Torben Braüner |
A Simple Adequate Categorical Model for PCF. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Stefano Berardi, Luca Boerio |
Minimum Information Code in a Pure Functional Language with Data Types. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Antonio Bucciarelli |
Logical Reconstruction of Bi-domains. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Christian Retoré |
Pomset Logic: A Non-commutative Extension of Classical Linear Logic. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Femke van Raamsdonk |
Outermost-Fair Rewriting. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Joëlle Despeyroux, Frank Pfenning, Carsten Schürmann |
Primitive Recursion for Higher-Order Abstract Syntax. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Stefano Guerrini, Simone Martini 0001, Andrea Masini |
Proof Nets, Garbage, and Computations. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Michael Brandt, Fritz Henglein |
Coinductive Axiomatization of Recursive Type Equality and Subtyping. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Viviana Bono, Michele Bugliesi |
Matching Constraints for the Lambda Calculus of Objects. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Yohji Akama |
A Lambda-to-CL Translation for Strong Normalization. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Jan Malolepszy, Malgorzata Moczurad, Marek Zaionc |
Schwichtenberg-Style Lambda Definability Is Undecidable. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Gianna Bellè, Eugenio Moggi |
Typed Intermediate Languages for Shape Analysis. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Neil Ghani |
Eta-Expansions in Dependent Type Theory - The Calculus of Constructions. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | Hongwei Xi |
Weak and Strong Beta Normalisations in Typed Lambda-Calculi. |
TLCA |
1997 |
DBLP DOI BibTeX RDF |
|
1 | M. Randall Holmes |
Untyped lambda-Calculus with Relative Typing. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Vincent Padovani |
On Equivalence Classes of Interpolation Equations. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Alberto Pravato, Simona Ronchi Della Rocca, Luca Roversi |
Categorical semantics of the call-by-value lambda-calculus. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Antonius J. C. Hurkens |
A Simplification of Girard's Paradox. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Healfdene Goguen |
Typed Operational Semantics. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Neil Ghani |
ßn-Equality for Coproducts. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Yann Coscoy, Gilles Kahn, Laurent Théry |
Extracting Text from Proofs. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Toshihiko Kurata, Masako Takahashi |
Decidable Properties of Intersection Type Systems. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Gavin M. Bierman |
What is a Categorical Model of Intuitionistic Linear Logic? |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Barthe |
Extensions of Pure Type Systems. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Furio Honsell, Marina Lenisa |
Final Semantics for untyped lambda-calculus. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Roberto Di Cosmo, Adolfo Piperno |
Expanding Extensional Polymorphism. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | 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 |
|
1 | Robert Pollack |
A Verified Typechecker. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Stefano Berardi, Marc Bezem, Thierry Coquand |
A realization of the negative interpretation of the Axiom of Choice. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Hidetaka Kondoh |
Basic Properties of Data Types with Inequational Refinements. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Jan Springintveld |
Third-Order Matching in the Presence of Type Constructors. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Dowek |
Lambda-calculus, Combinators and the Comprehension Scheme. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Stefano Berardi, Luca Boerio |
Using Subtyping in Program Optimization. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Alex K. Simpson |
Categorical completeness results for the simply-typed lambda-calculus. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Joëlle Despeyroux, Amy P. Felty, André Hirschowitz |
Higher-Order Abstract Syntax in Coq. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Jaco van de Pol, Helmut Schwichtenberg |
Strict Functionals for Termination Proofs. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Philippe de Groote |
A Simple Calculus of Exception Handling. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Daniel Briaud |
An explicit Eta rewrite rule. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Martin Hofmann 0001 |
A Simple Model for Quotient Types. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Andrea Asperti, Cosimo Laneve |
Comparing Lambda-calculus translations in Sharing Graphs. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Paul-André Melliès |
Typed lambda-calculi with explicit substitutions may not terminate. |
TLCA |
1995 |
DBLP DOI BibTeX RDF |
|
1 | Hans Leiß |
Combining Recursive and Dynamic Types. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
1 | Jan Springintveld |
Lower and Upper Bounds for Reductions of Types in Lambda-omega and Lambda-P. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
1 | Pietro Di Gianantonio, Furio Honsell |
An Abstract Notion of Application. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
1 | J. M. E. Hyland, C.-H. Luke Ong |
Modified Realizability Toposes and Strong Normalization Proofs. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
1 | Tobias Nipkow |
Orthogonal Higher-Order Rewrite Systems are Confluent. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
1 | Gilles Dowek |
The Undecidability of Typability in the Lambda-Pi-Calculus. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
1 | Franco Barbanera, Stefano Berardi |
Extracting Constructive Content from Classical Logic via Control-like Reductions. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
1 | Giorgio Ghelli |
Recursive Types Are not Conservative over F. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|
1 | Benjamin C. Pierce |
Intersection Types and Bounded Polymorphism. |
TLCA |
1993 |
DBLP DOI BibTeX RDF |
|