Search results for "TLCA"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	Benedetto Intrigila, Richard Statman	The Omega Rule is P11-Complete in the lambdabeta -Calculus.	TLCA	2007	DBLP DOI BibTeX RDF
1	Olha Shkaravska, Ron van Kesteren, Marko C. J. D. van Eekelen	Polynomial Size Analysis of First-Order Functions.	TLCA	2007	DBLP DOI BibTeX RDF	Shapely Functions, Size Analysis, Type Checking, Diophantine equations
1	Makoto Tatsuta	Simple Saturated Sets for Disjunction and Second-Order Existential Quantification.	TLCA	2007	DBLP DOI BibTeX RDF
1	René David, Karim Nour	An Arithmetical Proof of the Strong Normalization for the lambda -Calculus with Recursive Equations on Types.	TLCA	2007	DBLP DOI BibTeX RDF
1	Simona Ronchi Della Rocca (eds.)	Typed Lambda Calculi and Applications, 8th International Conference, TLCA 2007, Paris, France, June 26-28, 2007, Proceedings	TLCA	2007	DBLP DOI BibTeX RDF
1	Marcelo P. Fiore	Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic.	TLCA	2007	DBLP DOI BibTeX RDF
1	Sam Lindley	Extensional Rewriting with Sums.	TLCA	2007	DBLP DOI BibTeX RDF
1	Koji Nakazawa	An Isomorphism Between Cut-Elimination Procedure and Proof Reduction.	TLCA	2007	DBLP DOI BibTeX RDF
1	José Espírito Santo, Ralph Matthes, Luís Pinto 0001	Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi.	TLCA	2007	DBLP DOI BibTeX RDF
1	Patrick Baillot	From Proof-Nets to Linear Logic Type Systems for Polynomial Time Computing.	TLCA	2007	DBLP DOI BibTeX RDF
1	Denis Cousineau 0002, Gilles Dowek	Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo.	TLCA	2007	DBLP DOI BibTeX RDF
1	Stefano Berardi	Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves.	TLCA	2007	DBLP DOI BibTeX RDF
1	Andreas Abel 0001	Strong Normalization and Equi-(Co)Inductive Types.	TLCA	2007	DBLP DOI BibTeX RDF
1	William Blum, C.-H. Luke Ong	The Safe Lambda Calculus.	TLCA	2007	DBLP DOI BibTeX RDF
1	Ying Jiang, Guo-Qiang Zhang 0001	Weakly Distributive Domains.	TLCA	2007	DBLP DOI BibTeX RDF
1	Frank Pfenning	On a Logical Foundation for Explicit Substitutions.	TLCA	2007	DBLP DOI BibTeX RDF
1	Patricia Johann, Neil Ghani	Initial Algebra Semantics Is Enough!	TLCA	2007	DBLP DOI BibTeX RDF
1	James Lipton, Susana Nieva	Higher-Order Logic Programming Languages with Constraints: A Semantics.	TLCA	2007	DBLP DOI BibTeX RDF
1	Dimitris Mostrous, Nobuko Yoshida	Two Session Typing Systems for Higher-Order Mobile Processes.	TLCA	2007	DBLP DOI BibTeX RDF
1	Sylvain Boulmé	Intuitionistic Refinement Calculus.	TLCA	2007	DBLP DOI BibTeX RDF
1	Jean-Yves Marion	Predicative Analysis of Feasibility and Diagonalization.	TLCA	2007	DBLP DOI BibTeX RDF
1	Lionel Vaux	Convolution λ̅μ-Calculus.	TLCA	2007	DBLP DOI BibTeX RDF
1	Paula Severi, Fer-Jan de Vries	Continuity and Discontinuity in Lambda Calculus.	TLCA	2005	DBLP DOI BibTeX RDF
1	Pawel Urzyczyn (eds.)	Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings	TLCA	2005	DBLP DOI BibTeX RDF
1	Thierry Coquand	Completeness Theorems and lambda-Calculus.	TLCA	2005	DBLP DOI BibTeX RDF
1	Sam Lindley, Ian Stark	Reducibility and TT-Lifting for Computation Types.	TLCA	2005	DBLP DOI BibTeX RDF
1	Virgile Prevosto, Sylvain Boulmé	Proof Contexts with Late Binding.	TLCA	2005	DBLP DOI BibTeX RDF
1	Ken-etsu Fujita	Galois Embedding from Polymorphic Types into Existential Types.	TLCA	2005	DBLP DOI BibTeX RDF
1	Peter Selinger, Benoît Valiron	A Lambda Calculus for Quantum Computation with Classical Control.	TLCA	2005	DBLP DOI BibTeX RDF
1	François Lamarche, Lutz Straßburger	Naming Proofs in Classical Propositional Logic.	TLCA	2005	DBLP DOI BibTeX RDF
1	Christian Urban, James Cheney	Avoiding Equivariance in Alpha-Prolog.	TLCA	2005	DBLP DOI BibTeX RDF
1	Carsten Schürmann 0001, Adam Poswolsky, Jeffrey Sarnat	The [triangle]-Calculus. Functional Programming with Higher-Order Encodings.	TLCA	2005	DBLP DOI BibTeX RDF
1	Nick Benton, Benjamin Leperchey	Relational Reasoning in a Nominal Semantics for Storage.	TLCA	2005	DBLP DOI BibTeX RDF
1	René David, Karim Nour	Arithmetical Proofs of Strong Normalization Results for the Symmetric lambda-µ-Calculus.	TLCA	2005	DBLP DOI BibTeX RDF
1	Stan Matwin, Amy P. Felty, István T. Hernádvölgyi, Venanzio Capretta	Privacy in Data Mining Using Formal Methods.	TLCA	2005	DBLP DOI BibTeX RDF
1	François-Régis Sinot	Call-by-Name and Call-by-Value as Token-Passing Interaction Nets.	TLCA	2005	DBLP DOI BibTeX RDF
1	Susumu Hayashi	Can Proofs Be Animated By Games?	TLCA	2005	DBLP DOI BibTeX RDF
1	Ana Bove, Venanzio Capretta	Recursive Functions with Higher Order Domains.	TLCA	2005	DBLP DOI BibTeX RDF
1	Andreas Abel 0001, Thierry Coquand	Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs.	TLCA	2005	DBLP DOI BibTeX RDF
1	Damiano Zanardini	Higher-Order Abstract Non-interference.	TLCA	2005	DBLP DOI BibTeX RDF
1	Klaus Aehlig, Jolie G. de Miranda, C.-H. Luke Ong	The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidable.	TLCA	2005	DBLP DOI BibTeX RDF
1	Patrick Baillot, Kazushige Terui	A Feasible Algorithm for Typing in Elementary Affine Logic.	TLCA	2005	DBLP DOI BibTeX RDF
1	James Laird	The Elimination of Nesting in SPCF.	TLCA	2005	DBLP DOI BibTeX RDF
1	Ferruccio Damiani	Rank-2 Intersection and Polymorphic Recursion.	TLCA	2005	DBLP DOI BibTeX RDF
1	Greg Morrisett, Amal J. Ahmed 0001, Matthew Fluet	L3: A Linear Language with Locations.	TLCA	2005	DBLP DOI BibTeX RDF
1	John Power, Miki Tanaka	Binding Signatures for Generic Contexts.	TLCA	2005	DBLP DOI BibTeX RDF
1	Olivier Hermant	Semantic Cut Elimination in the Intuitionistic Sequent Calculus.	TLCA	2005	DBLP DOI BibTeX RDF	intuitionistic sequent calculus, cut admissibility, cut elimination property, semantic, Kripke Structure, deduction modulo
1	Gilles Barthe, Benjamin Grégoire, Fernando Pastawski	Practical Inference for Type-Based Termination in a Polymorphic Setting.	TLCA	2005	DBLP DOI BibTeX RDF
1	Paolo Coppola 0001, Ugo Dal Lago, Simona Ronchi Della Rocca	Elementary Affine Logic and the Call-by-Value Lambda Calculus.	TLCA	2005	DBLP DOI BibTeX RDF
1	Yves Bertot	Filters on CoInductive Streams, an Application to Eratosthenes' Sieve.	TLCA	2005	DBLP DOI BibTeX RDF
1	Amy P. Felty	A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code: Abstract.	TLCA	2005	DBLP DOI BibTeX RDF
1	Hugo Herbelin	On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic.	TLCA	2005	DBLP DOI BibTeX RDF
1	Roberto Di Cosmo, François Pottier, Didier Rémy	Subtyping Recursive Types Modulo Associative Commutative Products.	TLCA	2005	DBLP DOI BibTeX RDF
1	Michael Gordon Abbott, Thorsten Altenkirch, Neil Ghani, Conor McBride	Derivatives of Containers.	TLCA	2003	DBLP DOI BibTeX RDF
1	Ken-etsu Fujita	A Sound and Complete CPS-Translation for lambda-mu-Calculus.	TLCA	2003	DBLP DOI BibTeX RDF
1	John Power	A Universal Embedding for the Higher Order Structure of Computational Effects.	TLCA	2003	DBLP DOI BibTeX RDF
1	Paolo Coppola 0001, Simona Ronchi Della Rocca	Principal Typing in Elementary Affine Logic.	TLCA	2003	DBLP DOI BibTeX RDF
1	Frédéric Blanqui	Inductive Types in the Calculus of Algebraic Constructions.	TLCA	2003	DBLP DOI BibTeX RDF
1	Roberto M. Amadio	Max-Plus Quasi-interpretations.	TLCA	2003	DBLP DOI BibTeX RDF	Functional languages and term rewriting, Function algebras and implicit computational complexity, Polynomial interpretations and max-plus algebras, Static analysis
1	Nicolas Oury	Observational Equivalence and Program Extraction in the Coq Proof Assistant.	TLCA	2003	DBLP DOI BibTeX RDF
1	James Laird	A Fully Abstract Bidomain Model of Unary FPC.	TLCA	2003	DBLP DOI BibTeX RDF
1	Thierry Joly	Encoding of the Halting Problem into the Monster Type & Applications.	TLCA	2003	DBLP DOI BibTeX RDF
1	Jo Erskine Hannay	Abstraction Barrier-Observing Relational Parametricity.	TLCA	2003	DBLP DOI BibTeX RDF
1	Raphaël Montelatici	Polarized Proof Nets with Cycles and Fixpoints Semantics.	TLCA	2003	DBLP DOI BibTeX RDF
1	Andreas Abel 0001	Termination and Productivity Checking with Continuous Types.	TLCA	2003	DBLP DOI BibTeX RDF
1	Martin Hofmann 0001 (eds.)	Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings.	TLCA	2003	DBLP DOI BibTeX RDF
1	Antonio Bucciarelli, Benjamin Leperchey, Vincent Padovani	Relative Definability and Models of Unary PCF.	TLCA	2003	DBLP DOI BibTeX RDF
1	Stefan Kahrs	Well-Going Programs Can Be Typed.	TLCA	2003	DBLP DOI BibTeX RDF
1	Ranko Lazic 0001, David Nowak	On a Semantic Definition of Data Independence .	TLCA	2003	DBLP DOI BibTeX RDF	nondeterminism, logical relations, Data independence, definability
1	Thierry Coquand, Randy Pollack, Makoto Takeyama	A Logical Framework with Dependently Typed Records.	TLCA	2003	DBLP DOI BibTeX RDF
1	José Espírito Santo, Luís Pinto 0001	Permutative Conversions in Intuitionistic Multiary Sequent Calculi with Cuts.	TLCA	2003	DBLP DOI BibTeX RDF
1	Gérard Boudol	On Strong Normalization in the Intersection Type Discipline.	TLCA	2003	DBLP DOI BibTeX RDF
1	Michal Konecný	Functional In-Place Update with Layered Datatype Sharing.	TLCA	2003	DBLP DOI BibTeX RDF
1	François Maurel	Nondeterministic Light Logics and NP-Time.	TLCA	2003	DBLP DOI BibTeX RDF	Light logics, implicit characterisations of complexity classes, NP complexity
1	Yoshihiko Kakutani, Masahito Hasegawa	Parameterizations and Fixed-Point Operators on Control Categories.	TLCA	2003	DBLP DOI BibTeX RDF
1	Pietro Di Gianantonio	Game Semantics for the Pure Lazy lambda-calculus.	TLCA	2001	DBLP DOI BibTeX RDF
1	Norman Danner	Ramified Recurrence with Dependent Types.	TLCA	2001	DBLP DOI BibTeX RDF
1	James Laird	A Deconstruction of Non-deterministic Classical Cut Elimination.	TLCA	2001	DBLP DOI BibTeX RDF
1	Andrzej Filinski	Normalization by Evaluation for the Computational Lambda-Calculus.	TLCA	2001	DBLP DOI BibTeX RDF
1	Juliusz Chroboczek	Subtyping Recursive Games.	TLCA	2001	DBLP DOI BibTeX RDF
1	Herman Geuvers	Induction Is Not Derivable in Second Order Dependent Type Theory.	TLCA	2001	DBLP DOI BibTeX RDF
1	Christian Urban	Strong Normalisation for a Gentzen-like Cut-Elimination Procedure.	TLCA	2001	DBLP DOI BibTeX RDF	Recursive Path Ordering, Cut-Elimination, Explicit Substitution, Classical Logic
1	Samson Abramsky (eds.)	Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001, Krakow, Poland, May 2-5, 2001, Proceedings.	TLCA	2001	DBLP DOI BibTeX RDF
1	Teodor Knapik, Damian Niwinski, Pawel Urzyczyn	Deciding Monadic Theories of Hyperalgebraic Trees.	TLCA	2001	DBLP DOI BibTeX RDF
1	Ralph Matthes	Parigot's Second Order lambda-mu-Calculus and Inductive Types.	TLCA	2001	DBLP DOI BibTeX RDF
1	Ugo de'Liguoro	Characterizing Convergent Terms in Object Calculi via Intersection Types.	TLCA	2001	DBLP DOI BibTeX RDF
1	Alexandre Miquel	The Implicit Calculus of Constructions.	TLCA	2001	DBLP DOI BibTeX RDF
1	Peter Selinger	Categorical Semantics of Control.	TLCA	2001	DBLP DOI BibTeX RDF
1	Thorsten Altenkirch	Representations of First Order Function Types as Terminal Coalgebras.	TLCA	2001	DBLP DOI BibTeX RDF
1	Thierry Joly	The Finitely Generated Types of the lambda-Calculus.	TLCA	2001	DBLP DOI BibTeX RDF
1	Martin Hofmann 0001	From Bounded Arithmetic to Memory Management: Use of Type Theory to Capture Complexity Classes and Space Behaviour.	TLCA	2001	DBLP DOI BibTeX RDF
1	C. Barry Jay	Distinguishing Data Structures and Functions: The Constructor Calculus and Functorial Types.	TLCA	2001	DBLP DOI BibTeX RDF
1	Philippe de Groote	Strong Normalization of Classical Natural Deduction with Disjunction.	TLCA	2001	DBLP DOI BibTeX RDF
1	Aleksy Schubert	The Complexity of beta-Reduction in Low Orders.	TLCA	2001	DBLP DOI BibTeX RDF
1	Hans Leiß	Second-Order Pre-Logical Relations and Representation Independence.	TLCA	2001	DBLP DOI BibTeX RDF
1	Esfandiar Haghverdi	Partially Additive Categories and Fully Complete Models of Linear Logic.	TLCA	2001	DBLP DOI BibTeX RDF
1	Dag Normann	Definability of Total Objects in PCF and Related Calculi.	TLCA	2001	DBLP DOI BibTeX RDF
1	Daniel J. Dougherty, Pierre Lescanne	Reductions, Intersection Types, and Explicit Substitutions.	TLCA	2001	DBLP DOI BibTeX RDF
1	Gilles Dowek	The Stratified Foundations as a Theory Modulo.	TLCA	2001	DBLP DOI BibTeX RDF
1	Olivier Laurent 0001	A Token Machine for Full Geometry of Interaction.	TLCA	2001	DBLP DOI BibTeX RDF

Publications at "TLCA"( http://dblp.L3S.de/Venues/TLCA )