Typed Lambda Calculus and Applications
2005
- Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairsby: Andreas Abel, Thierry Coquand
- A Lambda Calculus for Quantum Computation with Classical Controlby: Peter Selinger, Benoit Valiron
- Elementary Affine Logic and the Call-by-Value Lambda Calculusby: Paolo Coppola, Ugo Dal Lago, Simona Ronchi Della Rocca
- Binding Signatures for Generic Contextsby: John Power, Miki Tanaka
- A Feasible Algorithm for Typing in Elementary Affine Logicby: Patrick Baillot, Kazushige Terui
- Semantic Cut Elimination in the Intuitionistic Sequent Calculusby: Olivier Hermant
- Galois Embedding from Polymorphic Types into Existential Typesby: Ken-etsu Fujita
- Arithmetical Proofs of Strong Normalization Results for the Symmetric lambda-µ-Calculusby: René David, Karim Nour
- Filters on CoInductive Streams, an Application to Eratosthenes' Sieveby: Yves Bertot
- Completeness Theorems and lambda-Calculusby: Thierry Coquand
- L3: A Linear Language with Locationsby: Greg Morrisett, Amal J. Ahmed, Matthew Fluet
- The Elimination of Nesting in SPCFby: James Laird
- Subtyping Recursive Types Modulo Associative Commutative Productsby: Roberto Di Cosmo, François Pottier, Didier Rémy
- Continuity and Discontinuity in Lambda Calculusby: Paula Severi, Fer-Jan de Vries
- Privacy in Data Mining Using Formal Methodsby: Stan Matwin, Amy P. Felty, István T. Hernádvölgyi, Venanzio Capretta
- Reducibility and TT-Lifting for Computation Typesby: Sam Lindley, Ian Stark
- Proof Contexts with Late Bindingby: Virgile Prevosto, Sylvain Boulmé
- Avoiding Equivariance in Alpha-Prologby: Christian Urban, James Cheney
- Recursive Functions with Higher Order Domainsby: Ana Bove, Venanzio Capretta
- Practical Inference for Type-Based Termination in a Polymorphic Settingby: Gilles Barthe, Benjamin Grégoire, Fernando Pastawski
- Naming Proofs in Classical Propositional Logicby: François Lamarche, Lutz Straßburger
- Relational Reasoning in a Nominal Semantics for Storageby: Nick Benton, Benjamin Leperchey
- Rank-2 Intersection and Polymorphic Recursionby: Ferruccio Damiani
- Call-by-Name and Call-by-Value as Token-Passing Interaction Netsby: François-Régis Sinot
- The Monadic Second Order Theory of Trees Given by Arbitrary Level-Two Recursion Schemes Is Decidableby: Klaus Aehlig, Jolie G. de Miranda, C.-H. Luke Ong
- A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code: Abstractby: Amy P. Felty
- Higher-Order Abstract Non-interferenceby: Damiano Zanardini
- On the Degeneracy of Sigma-Types in Presence of Computational Classical Logicby: Hugo Herbelin
- Can Proofs Be Animated By Games?by: Susumu Hayashi
- The [triangle]-Calculus. Functional Programming with Higher-Order Encodingsby: Carsten Schürmann, Adam Poswolsky, Jeffrey Sarnat
- A Logical Framework with Dependently Typed Recordsby: Thierry Coquand, Randy Pollack, Makoto Takeyama
- Encoding of the Halting Problem into the Monster Type & Applicationsby: Thierry Joly
- Abstraction Barrier-Observing Relational Parametricityby: Jo Erskine Hannay
- Principal Typing in Elementary Affine Logicby: Paolo Coppola, Simona Ronchi Della Rocca
- Observational Equivalence and Program Extraction in the Coq Proof Assistantby: Nicolas Oury
- Nondeterministic Light Logics and NP-Timeby: François Maurel
- A Universal Embedding for the Higher Order Structure of Computational Effectsby: John Power
- Well-Going Programs Can Be Typedby: Stefan Kahrs
- Functional In-Place Update with Layered Datatype Sharingby: Michal Konecný
- A Fully Abstract Bidomain Model of Unary FPCby: James Laird
- Max-Plus Quasi-interpretationsby: Roberto M. Amadio
- Polarized Proof Nets with Cycles and Fixpoints Semanticsby: Raphaël Montelatici
- Parameterizations and Fixed-Point Operators on Control Categoriesby: Yoshihiko Kakutani, Masahito Hasegawa
- On Strong Normalization in the Intersection Type Disciplineby: Gérard Boudol
- On a Semantic Definition of Data Independence by: Ranko Lazic, David Nowak
- Inductive Types in the Calculus of Algebraic Constructionsby: Frédéric Blanqui
- Relative Definability and Models of Unary PCFby: Antonio Bucciarelli, Benjamin Leperchey, Vincent Padovani
- A Sound and Complete CPS-Translation for lambda-mu-Calculusby: Ken-etsu Fujita
- Permutative Conversions in Intuitionistic Multiary Sequent Calculi with Cutsby: José Espírito Santo, Luis Pinto
- Derivatives of Containersby: Michael Abbott, Thorsten Altenkirch, Neil Ghani, Conor McBride
- Termination and Productivity Checking with Continuous Typesby: Andreas Abel
- Strong Normalization of Classical Natural Deduction with Disjunctionby: Philippe de Groote
- Strong Normalisation for a Gentzen-like Cut-Elimination Procedureby: Christian Urban
- The Complexity of beta-Reduction in Low Ordersby: Aleksy Schubert
- Characterizing Convergent Terms in Object Calculi via Intersection Typesby: Ugo de'Liguoro
- Distinguishing Data Structures and Functions: The Constructor Calculus and Functorial Typesby: C. Barry Jay
- The Finitely Generated Types of the lambda-Calculusby: Thierry Joly
- Typing Lambda Terms in Elementary Logic with Linear Constraintsby: Paolo Coppola, Simone Martini
- Retracts in Simple Typesby: Vincent Padovani
- Parallel Implementation Models for the lambda-Calculus Using the Geometry of Interactionby: Jorge Sousa Pinto
- Parigot's Second Order lambda-mu-Calculus and Inductive Typesby: Ralph Matthes
- The Implicit Calculus of Constructionsby: Alexandre Miquel
- Many Happy Returnsby: Olivier Danvy
- Reductions, Intersection Types, and Explicit Substitutionsby: Daniel J. Dougherty, Pierre Lescanne
- A Finitary Subsystem of the Polymorphic lambda-Calculusby: Thorsten Altenkirch, Thierry Coquand
- Induction Is Not Derivable in Second Order Dependent Type Theoryby: Herman Geuvers
- Deciding Monadic Theories of Hyperalgebraic Treesby: Teodor Knapik, Damian Niwinski, Pawel Urzyczyn
- A Deconstruction of Non-deterministic Classical Cut Eliminationby: James Laird
- Logical Properties of Name Restrictionby: Luca Cardelli, Andrew D. Gordon
- The Stratified Foundations as a Theory Moduloby: Gilles Dowek
- Second-Order Pre-Logical Relations and Representation Independenceby: Hans Leiß
- Subtyping Recursive Gamesby: Juliusz Chroboczek
- From Bounded Arithmetic to Memory Management: Use of Type Theory to Capture Complexity Classes and Space Behaviourby: Martin Hofmann
- Partially Additive Categories and Fully Complete Models of Linear Logicby: Esfandiar Haghverdi
- Ramified Recurrence with Dependent Typesby: Norman Danner
- Representations of First Order Function Types as Terminal Coalgebrasby: Thorsten Altenkirch
- Definability of Total Objects in PCF and Related Calculiby: Dag Normann
- A Token Machine for Full Geometry of Interactionby: Olivier Laurent
- Evolving Games and Essential Nets for Affine Polymorphismby: Andrzej S. Murawski, C.-H. Luke Ong
- Game Semantics for the Pure Lazy lambda-calculusby: Pietro Di Gianantonio
- Normalization by Evaluation for the Computational Lambda-Calculusby: Andrzej Filinski
- Sequentiality and the pi-Calculusby: Martin Berger, Kohei Honda, Nobuko Yoshida
- Categorical Semantics of Controlby: Peter Selinger
- Counting a Type's Principal Inhabitantsby: Sabine Broda, Luís Damas
- A Curry-Howard Isomorphism for Compilation and Program Executionby: Atsushi Ohori
- Elementary Complexity and Geometry of Interactionby: Patrick Baillot, Marco Pedicini
- Lambda Definability with Sums via Grothendieck Logical Relationsby: Marcelo P. Fiore, Alex K. Simpson
- Call-by-Push-Value: A Subsuming Paradigmby: Paul Blain Levy
- Quantitative Semantics Revisitedby: Nuno Barreiro, Thomas Ehrhard
- Total Functionals and Well-Founded Strategiesby: Stefano Berardi, Ugo de'Liguoro
- A Logic for Abstract Data Types as Existential Typesby: Erik Poll, Jan Zwanenburg
- Game Semantics for Untyped lambda beta eta-Calculusby: Pietro Di Gianantonio, Gianluca Franco, Furio Honsell
- Strong Normalisation of Cut-Elimination in Classical Logicby: C. Urban, Gavin M. Bierman
- Pure Type Systems with Subtypingby: Jan Zwanenburg
- Every Unsolvable lambda Term has a Decorationby: René David
- Consequences of Jacopini's Theorem: Consistent Equalities and Equationsby: Richard Statman
- A Study of Abramsky's Linear Chemical Abstract Machineby: Seikoh Mikami, Yohji Akama
- Characterising Explicit Substitutions which Preserve Terminationby: Eike Ritter
- Soundness of the Logical Framework for Its Typed Operational Semanticsby: Healfdene Goguen
- AnnoDomini in Practice: A Type-Theoretic Approach to the Year 2000 Problemby: Peter Harry Eidorff, Fritz Henglein, Christian Mossin, Henning Niss, Morten Heine Sørensen, Mads Tofte
- Logical Predicates for Intuitionistic Linear Type Theoriesby: Masahito Hasegawa
- Resource Interpretations, Bunched Implications and the alpha lambda-Calculusby: Peter W. O'Hearn
- Natural Deduction for Intuitionistic Non-communicative Linear Logicby: Jeff Polakow, Frank Pfenning
- Modules in Non-communicative Logicby: V. Michele Abrusci
- Polarized Proof-Nets: Proof-Nets for LCby: Olivier Laurent
- Explicitly Typed lambda µ-Calculus for Polymorphism an Call-by-Valueby: Ken-etsu Fujita
- A Finite Axiomatization of Inductive-Recursive Definitionsby: Peter Dybjer, Anton Setzer
- Explicit Environmentsby: Masahiko Sato, Takafumi Sakurai, Rod M. Burstall
- Useless-Code Detection and Elimination for PCF with Algebraic Data typesby: Ferruccio Damiani
- The Coordination Language Facility and Applicationsby: Jean-Marc Andreoli
- Weak and Strong Beta Normalisations in Typed Lambda-Calculiby: Hongwei Xi
- A Lambda-to-CL Translation for Strong Normalizationby: Yohji Akama
- A Module Calculus for Pure Type Systemsby: Judicaël Courant
- Semantic Techniques for Deriving Coinductive Characterizations of Observational Equivalences for Lambda-calculiby: Marina Lenisa
- Typed Intermediate Languages for Shape Analysisby: Gianna Bellè, Eugenio Moggi
- Schwichtenberg-Style Lambda Definability Is Undecidableby: Jan Malolepszy, Malgorzata Moczurad, Marek Zaionc
- Matching Constraints for the Lambda Calculus of Objectsby: Viviana Bono, Michele Bugliesi
- Minimum Information Code in a Pure Functional Language with Data Typesby: Stefano Berardi, Luca Boerio
- An Inference Algorithm for Strictnessby: Ferruccio Damiani, Paola Giannini
- Coinductive Axiomatization of Recursive Type Equality and Subtypingby: Michael Brandt, Fritz Henglein
- A Simple Adequate Categorical Model for PCFby: Torben Braüner
- Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic Lambda Calculiby: Masahito Hasegawa
- A Non-commutative Extension of Classical Linear Logicby: Christian Retoré, Pomset Logic
- Logical Reconstruction of Bi-domainsby: Antonio Bucciarelli
- Primitive Recursion for Higher-Order Abstract Syntaxby: Joëlle Despeyroux, Frank Pfenning, Carsten Schürmann
- Computational Reflection in the Calculus of Constructions and its Application to Theorem Provingby: Harald Rueß
- Inhabitation in Typed Lambda-Calculi (A Syntactic Approach)by: Pawel Urzyczyn
- Games and Weak-Head Reduction for Classical PCFby: Hugo Herbelin
- Names, Equations, Relations: Practical Ways to Reason about newby: Ian Stark
- An Axiomatic System of Parametricityby: Izumi Takeuti
- Eta-Expansions in Dependent Type Theory - The Calculus of Constructionsby: Neil Ghani
- Proof Nets, Garbage, and Computationsby: Stefano Guerrini, Simone Martini, Andrea Masini
- A Type Theoretical View of Böhm-Treesby: Toshihiko Kurata
- Outermost-Fair Rewritingby: Femke van Raamsdonk
- A Simplification of Girard's Paradoxby: Antonius J. C. Hurkens
- A Simple Calculus of Exception Handlingby: Philippe de Groote
- Extracting Text from Proofsby: Yann Coscoy, Gilles Kahn, Laurent Théry
- A Verified Typecheckerby: Robert Pollack
- Untyped lambda-Calculus with Relative Typingby: M. Randall Holmes
- On Equivalence Classes of Interpolation Equationsby: Vincent Padovani
- Strict Functionals for Termination Proofsby: Jaco van de Pol, Helmut Schwichtenberg
- Expanding Extensional Polymorphismby: Roberto Di Cosmo, Adolfo Piperno
- Using Subtyping in Program Optimizationby: Stefano Berardi, Luca Boerio
- Final Semantics for untyped lambda-calculusby: Furio Honsell, Marina Lenisa
- Third-Order Matching in the Presence of Type Constructorsby: Jan Springintveld
- Categorical completeness results for the simply-typed lambda-calculusby: Alex K. Simpson
- Comparing Lambda-calculus translations in Sharing Graphsby: Andrea Asperti, Cosimo Laneve
- Termination Proof of Term Rewriting System with the Multiset Path Ordering. A Complete Development in the System Coqby: François Leclerc
- Typed Operational Semanticsby: Healfdene Goguen
- Lambda-calculus, Combinators and the Comprehension Schemeby: Gilles Dowek
- What is a Categorical Model of Intuitionistic Linear Logic?by: Gavin M. Bierman
- Higher-Order Abstract Syntax in Coqby: Joëlle Despeyroux, Amy P. Felty, André Hirschowitz
- A Simple Model for Quotient Typesby: Martin Hofmann
- Extensions of Pure Type Systemsby: Gilles Barthe
- Decidable Properties of Intersection Type Systemsby: Toshihiko Kurata, Masako Takahashi
- A Model for Formal Parametric Polymorphism: A PER Interpretation for System Rby: Roberto Bellucci, Martín Abadi, Pierre-Louis Curien
- Typed lambda-calculi with explicit substitutions may not terminateby: Paul-André Melliès
- A realization of the negative interpretation of the Axiom of Choiceby: Stefano Berardi, Marc Bezem, Thierry Coquand
- ßn-Equality for Coproductsby: Neil Ghani
- Categorical semantics of the call-by-value lambda-calculusby: Alberto Pravato, Simona Ronchi Della Rocca, Luca Roversi
- Basic Properties of Data Types with Inequational Refinementsby: Hidetaka Kondoh
- A Fully Abstract Translation between a Lambda-Calculus with Reference Types and Standard MLby: Eike Ritter, Andrew M. Pitts
- An explicit Eta rewrite ruleby: Daniel Briaud
- On Mints' Reduction for ccc-Calculusby: Yohji Akama
- The Conservation Theorem revisitedby: Philippe de Groote
- Partial Intersection Type Assignment in Applicative Term Rewriting Systemsby: Steffen van Bakel
- Intersection Types and Bounded Polymorphismby: Benjamin C. Pierce
- Lambda calculus characterizations of poly-timeby: Daniel Leivant, Jean-Yves Marion
- Program Extraction from Normalization Proofsby: Ulrich Berger
- Extracting Constructive Content from Classical Logic via Control-like Reductionsby: Franco Barbanera, Stefano Berardi
- Combining First and Higher Order Rewrite Systems with Type Assignment Systemsby: Franco Barbanera, Maribel Fernández
- Semantics of lambda-I and of other substructure lambda calculiby: Bart Jacobs
- Monotonic versus Antimonotonic Exponentationby: Daniel F. Otth
- Lambda-Calculi with Conditional Rulesby: Masako Takahashi
- Pure Type Systems Formalizedby: James McKinna, Robert Pollack
- Modified Realizability Toposes and Strong Normalization Proofsby: J. M. E. Hyland, C.-H. Luke Ong
- Recursive Types Are not Conservative over Fby: Giorgio Ghelli
- Lower and Upper Bounds for Reductions of Types in Lambda-omega and Lambda-Pby: Jan Springintveld
- Studying the Fully Abstract Model of PCF within its Continuous Function Modelby: Achim Jung, Allen Stoughton
- A New Characterization of Lambda Definabilityby: Achim Jung, Jerzy Tiuryn
- A Term Calculus for Intuitionistic Linear Logicby: P. N. Benton, Gavin M. Bierman, Valeria de Paiva, Martin Hyland
- The Undecidability of Typability in the Lambda-Pi-Calculusby: Gilles Dowek
- Combining Recursive and Dynamic Typesby: Hans Leiß
- A Logic for Parametric Polymorphismby: Gordon D. Plotkin, Martín Abadi
- Type reconstruction in F-omega is undecidableby: Pawel Urzyczyn
- An Abstract Notion of Applicationby: Pietro Di Gianantonio, Furio Honsell
- A Formalization of the Strong Normalization Proof for System F in LEGOby: Thorsten Altenkirch
- Call-by-Value and Nondeterminismby: Kurt Sieber
- Orthogonal Higher-Order Rewrite Systems are Confluentby: Tobias Nipkow
- A Semantics for Lambda&-early: A Calculus with Overloading and Early Bindingby: Giuseppe Castagna, Giorgio Ghelli, Giuseppe Longo
- Inductive Definitions in the system Coq - Rules and Propertiesby: Christine Paulin-Mohring
- Translating Dependent Type Theory into Higher Order Logicby: Bart Jacobs, Thomas F. Melham
![[SWISH++]](/docis/swish-powered.gif){kind=small}
