Tag #λ-calculus
283 papers:
POPL-2020-BrunelMP #linear- Backpropagation in the simply typed lambda-calculus with linear negation (AB, DM, MP), p. 27.
- POPL-2020-ClairambaultV #abstraction #quantum
- Full abstraction for the quantum lambda-calculus (PC, MdV), p. 28.
- POPL-2020-ForsterKR #call-by
- The weak call-by-value λ-calculus is reasonable for both time and space (YF0, FK, MR), p. 23.
CSL-2020-Santo #call-by- The Call-By-Value Lambda-Calculus with Generalized Applications (JES), p. 12.
FSCD-2019-Accattoli #fresh look- A Fresh Look at the lambda-Calculus (Invited Talk) (BA), p. 20.
- FSCD-2019-Bendkowski #analysis #towards
- Towards the Average-Case Analysis of Substitution Resolution in Lambda-Calculus (MB), p. 21.
- FSCD-2019-KasterovicP #call-by #lazy evaluation #power of #probability
- The Discriminating Power of the Let-In Operator in the Lazy Call-by-Name Probabilistic lambda-Calculus (SK, MP), p. 20.
- FSCD-2019-LagoL #on the #probability
- On the Taylor Expansion of Probabilistic lambda-terms (UDL, TL), p. 16.
- ICFP-2019-Morihata #algebra #equation #parallel #reasoning #reduction
- Lambda calculus with algebraic simplification for reduction parallelization by equational reasoning (AM), p. 25.
PEPM-2019-Jay - A simpler lambda calculus (BJ), pp. 1–9.
PPDP-2019-0001S #call-by #evaluation #normalisation- Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda Calculus (AA0, CS), p. 12.
ESOP-2019-GiarrussoRS #incremental #program transformation- Incremental λ-Calculus in Cache-Transfer Style - Static Memoization by Program Transformation (PGG, YRG, PS), pp. 553–580.
- FSCD-2018-Bahr #strict
- Strict Ideal Completions of the Lambda Calculus (PB), p. 16.
PADL-2018-Tarau #on the- On k-colored Lambda Terms and Their Skeletons (PT), pp. 116–131.
- PPDP-2018-BreuvartL #on the #probability
- On Intersection Types and Probabilistic Lambda Calculi (FB, UDL), p. 13.
- ESOP-2018-0001BBBG0 #markov #probability #reasoning #relational
- Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus (AA0, GB, LB, AB, MG, DG0), pp. 214–241.
- CSL-2018-ClairambaultP #modelling #probability
- Fully Abstract Models of the Probabilistic lambda-calculus (PC, HP), p. 17.
- FSCD-2017-Akama #confluence #term rewriting
- The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type (YA), p. 19.
LOPSTR-2017-BodiniT #on the- On Uniquely Closable and Uniquely Typable Skeletons of Lambda Terms (OB, PT), pp. 252–268.
- PADL-2017-BendkowskiGT
- Boltzmann Samplers for Closed Simply-Typed Lambda Terms (MB, KG, PT), pp. 120–135.
- PEPM-2017-BerezunJ #compilation #game studies #partial evaluation #semantics
- Compiling untyped lambda calculus to lower-level code by game semantics and partial evaluation (invited paper) (DB, NDJ), pp. 1–11.
- PPDP-2017-SantoG
- Characterization of strong normalizability for a sequent lambda calculus with co-control (JES, SG), pp. 163–174.
- FSCD-2016-AkiyoshiT #normalisation #polymorphism
- Strong Normalization for the Parameter-Free Polymorphic Lambda Calculus Based on the Omega-Rule. (RA, KT), p. 15.
- ICFP-2016-BorgstromLGS #probability #programming
- A lambda-calculus foundation for universal probabilistic programming (JB, UDL, ADG, MS), pp. 33–46.
- ICFP-2016-Takeda0YS #encoding
- Compact bit encoding schemes for simply-typed lambda-terms (KT, NK0, KY, AS), pp. 146–157.
- LOPSTR-2016-Tarau #generative #normalisation #order #performance
- A Hiking Trip Through the Orders of Magnitude: Deriving Efficient Generators for Closed Simply-Typed Lambda Terms and Normal Forms (PT), pp. 240–255.
- PADL-2016-Tarau #encoding
- A Size-Proportionate Bijective Encoding of Lambda Terms as Catalan Objects Endowed with Arithmetic Operations (PT), pp. 99–116.
- PPDP-2016-EhrhardG #call-by
- The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value (TE, GG), pp. 174–187.
- ESOP-2016-FeltmanAAF #automation
- Automatically Splitting a Two-Stage Lambda Calculus (NF, CA, UAA, KF), pp. 255–281.
- CSL-2016-ParysT #logic #modelling
- Models of Lambda-Calculus and the Weak MSO Logic (PP, ST), p. 12.
TLCA-2015-GuerrieriPR #call-by #standard- Standardization of a Call-By-Value λ-Calculus (GG, LP, SRDR), pp. 211–225.
- TLCA-2015-Redmond #parametricity #polynomial
- Polynomial Time in the Parametric λ Calculus (BFR), pp. 288–301.
Haskell-2015-Polakow #haskell #linear- Embedding a full linear Lambda calculus in Haskell (JP), pp. 177–188.
ICFP-2015-GaboardiP #algebra- Algebras and coalgebras in the light affine λ calculus (MG, RP), pp. 114–126.
- POPL-2015-Tobisawa
- A Meta λ Calculus with Cross-Level Computation (KT), pp. 383–393.
FoSSaCS-2015-Winter #bisimulation #finite- A Completeness Result for Finite λ-bisimulations (JW), pp. 117–132.
LICS-2015-Munch-Maccagnoni #representation- Polarised Intermediate Representation of λ Calculus with Sums (GMM, GS), pp. 127–140.
ICALP-v2-2014-Mazza - Non-uniform Polytime Computation in the Infinitary Affine λ-Calculus (DM), pp. 305–317.
RTA-TLCA-2014-Czajka #confluence #induction #proving- A Coinductive Confluence Proof for Infinitary λ-Calculus (LC), pp. 164–178.
- RTA-TLCA-2014-NakazawaN #reduction #μ-calculus
- Reduction System for Extensional Λμ Calculus (KN, TN), pp. 349–363.
- RTA-TLCA-2014-Schmidt-SchaussS #call-by
- Applicative May- and Should-Simulation in the Call-by-Value λ Calculus with AMB (MSS, DS), pp. 379–394.
- RTA-TLCA-2014-Statman
- Near Semi-rings and λ Calculus (RS), pp. 410–424.
- ICFP-2014-GrabmayerR
- Maximal sharing in the λ calculus with letrec (CG, JR), pp. 67–80.
- PEPM-2014-Garcia-PerezNS
- Deriving interpretations of the gradually-typed λ calculus (ÁGP, PN, IS), pp. 157–168.
PLDI-2014-CaiGRO #difference #formal method #higher-order- A theory of changes for higher-order languages: incrementalizing λ-calculi by static differentiation (YC, PGG, TR, KO), p. 17.
- ESOP-2014-CrubilleL #bisimulation #call-by #on the #probability
- On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi (RC, UDL), pp. 209–228.
- ICALP-v2-2013-Stirling #proving
- Proof Systems for Retracts in Simply Typed λ Calculus (CS), pp. 398–409.
- RTA-2013-GrabmayerR #μ-calculus
- Expressibility in the λ Calculus with μ (CG, JR), pp. 206–222.
- RTA-2013-Schmidt-SchaussMS #lazy evaluation
- Extending Abramsky’s Lazy λ Calculus: (Non)-Conservativity of Embeddings (MSS, EM, DS), pp. 239–254.
- TLCA-2013-Breuvart #relational
- The Resource λ Calculus Is Short-Sighted in Its Relational Model (FB), pp. 93–108.
- CSL-2013-Kikuchi #nondeterminism #normalisation #proving
- Proving Strong Normalisation via Non-deterministic Translations into Klop’s Extended λ-Calculus (KK), pp. 395–414.
- LICS-2013-AspertiL #cost analysis
- The Cost of Usage in the λ-Calculus (AA, JJL), pp. 293–300.
- LICS-2013-GundersenHP
- Atomic λ Calculus: A Typed λ-Calculus with Explicit Sharing (TG, WH, MP), pp. 311–320.
- LICS-2013-LairdMMP #modelling #relational
- Weighted Relational Models of Typed λ-Calculi (JL, GM, GM, MP), pp. 301–310.
- RTA-2012-Terui #complexity #evaluation #semantics
- Semantic Evaluation, Intersection Types and Complexity of Simply Typed λ Calculus (KT), pp. 323–338.
FLOPS-2012-Hirai #logic- A λ Calculus for Gödel-Dummett Logic Capturing Waitfreedom (YH), pp. 151–165.
- ICFP-2012-ChenEW #type system
- An error-tolerant type system for variational λ calculus (SC, ME, EW), pp. 29–40.
- PPDP-2012-Madet #multi #polynomial #thread
- A polynomial time λ-calculus with multithreading and side effects (AM), pp. 55–66.
- ESOP-2012-ChangF #call-by #revisited
- The Call-by-Need λ Calculus, Revisited (SC, MF), pp. 128–147.
- CSL-2012-CarraroS #consistency #equation #formal method #modelling #on the
- On the equational consistency of order-theoretic models of the λ-calculus (AC, AS), pp. 152–166.
ICLP-J-2012-BaralDGG #algorithm #correctness #programming #set- Typed answer set programming λ calculus theories and correctness of inverse λ algorithms with respect to them (CB, JD, MAG, AG), pp. 775–791.
- LICS-2012-Klop #term rewriting
- Term Rewriting and λ Calculus (JWK), p. 12.
- LICS-2012-Mazza
- An Infinitary Affine λ-Calculus Isomorphic to the Full λ-Calculus (DM), pp. 471–480.
- RTA-2011-GrathwohlKPS #graph #named #reduction #term rewriting #visualisation
- Anagopos: A Reduction Graph Visualizer for Term Rewriting and λ Calculus (NBBG, JK, JDP, JGS), pp. 61–70.
- RTA-2011-SeveriV #axiom
- Weakening the Axiom of Overlap in Infinitary λ Calculus (PS, FJdV), pp. 313–328.
- TLCA-2011-BakelBd #μ-calculus
- A Filter Model for the λμ-Calculus — (SvB, FB, Ud), pp. 213–228.
- TLCA-2011-BourreauS #game studies #semantics
- Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus (PB, SS), pp. 61–75.
- TLCA-2011-MadetA #multi #thread
- An Elementary Affine λ-Calculus with Multithreading and Side Effects (AM, RMA), pp. 138–152.
- TLCA-2011-ManzonettoP #theorem
- Böhm’s Theorem for Resource λ Calculus through Taylor Expansion (GM, MP), pp. 153–168.
- TLCA-2011-Roversi #linear
- Linear λ Calculus and Deep Inference (LR), pp. 184–197.
- PPDP-2011-AlvesFFM #recursion
- Linearity and recursion in a typed λ-calculus (SA, MF, MF, IM), pp. 173–182.
- PPDP-2011-Guenot #proving #reduction
- Nested proof search as reduction in the λ-calculus (NG), pp. 183–194.
- CSL-2011-Ehrhard #difference
- Resource λ-Calculus: the Differential Viewpoint (TE), p. 1.
- RTA-2010-Schmidt-SchaussSM #call-by #simulation
- Simulation in the Call-by-Need λ-Calculus with letrec (MSS, DS, EM), pp. 295–310.
- FLOPS-2010-KetemaS #bound #diagrams #term rewriting
- Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus (JK, JGS), pp. 272–287.
- FLOPS-2010-Saurin #standard #μ-calculus
- Standardization and Böhm Trees for λμ-Calculus (AS), pp. 134–149.
- FoSSaCS-2010-PaganiR
- Solvability in Resource λ-Calculus (MP, SRDR), pp. 358–373.
- CSL-2010-AccattoliK
- The Structural λ-Calculus (BA, DK), pp. 381–395.
- ICLP-2010-Snow10
- Realizing the Dependently Typed λ Calculus (ZS), pp. 294–299.
IJCAR-2010-Schack-NielsenS #linear- Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus (ASN, CS), pp. 1–14.
- ICALP-v2-2009-LagoM #on the #term rewriting
- On Constructor Rewrite Systems and the λ-Calculus (UDL, SM), pp. 163–174.
- TLCA-2009-HerbelinZ #call-by #deduction
- An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form (HH, SZ), pp. 142–156.
- TLCA-2009-Petit #polymorphism #type system
- A Polymorphic Type System for the λ-Calculus with Constructors (BP), pp. 234–248.
- CSL-2009-Sumii #equivalence #polymorphism
- A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References (ES), pp. 455–469.
- LICS-2009-CarraroS #reflexive
- Reflexive Scott Domains are Not Complete for the Extensional λ Calculus (AC, AS), pp. 91–100.
- RTA-2008-ArrighiD #algebra #confluence #encoding #higher-order
- Linear-algebraic λ-calculus: higher-order, encodings, and confluence (PA, GD), pp. 17–31.
- RTA-2008-Schmidt-SchaussM #call-by #finite #nondeterminism #simulation
- A Finite Simulation Method in a Non-deterministic Call-by-Need λ-Calculus with Letrec, Constructors, and Case (MSS, EM), pp. 321–335.
- RTA-2008-Ueda #encoding #graph grammar
- Encoding the Pure λ Calculus into Hierarchical Graph Rewriting (KU), pp. 392–408.
- FoSSaCS-2008-GianantonioHL #higher-order
- RPO, Second-Order Contexts, and λ-Calculus (PDG, FH, ML), pp. 334–349.
- FoSSaCS-2008-SelingerV #call-by
- A Linear-non-Linear Model for a Computational Call-by-Value λ Calculus (PS, BV), pp. 81–96.
- CSL-2008-NakazawaTKN
- Undecidability of Type-Checking in Domain-Free Typed λ-Calculi with Existence (KN, MT, YK, HN), pp. 478–492.
- CSL-2008-Saurin #on the #μ-calculus
- On the Relations between the Syntactic Theories of λμ-Calculi (AS), pp. 154–168.
- RTA-2007-Tatsuta #μ-calculus
- The Maximum Length of μ-Reduction in λμ-Calculus (MT), pp. 359–373.
SEFM-2007-AlhadidiBDB #aspect-oriented- An AOP Extended λ-Calculus (DA, NB, MD, PB), pp. 183–194.
- TLCA-2007-BlumO
- The Safe λ Calculus (WB, CHLO), pp. 39–53.
- TLCA-2007-Vaux #μ-calculus
- Convolution λμ-Calculus (LV), pp. 381–395.
CEFP-2007-CsornyeiD - An Introduction to the λ Calculus (ZC, GD), pp. 87–111.
- CEFP-2007-Kluge
- Abstract λ-Calculus Machines (WEK), pp. 112–157.
- PLDI-2007-Chlipala #assembly #compilation
- A certified type-preserving compiler from λ calculus to assembly language (AC), pp. 54–65.
- POPL-2007-Murthy #design #enterprise #programming language
- Advanced programming language design in enterprise software: a λ-calculus theorist wanders into a datacenter (CM), pp. 263–264.
- ICALP-v2-2006-Levy
- Jumbo λ-Calculus (PBL), pp. 444–455.
- RTA-2006-ArbiserMR
- A λ-Calculus with Constructors (AA, AM, AR), pp. 181–196.
- RTA-2006-OhtaH #confluence #linear
- A Terminating and Confluent Linear λ Calculus (YO, MH), pp. 166–180.
- RTA-2006-Salvati #equation #linear #type system
- Syntactic Descriptions: A Type System for Solving Matching Equations in the Linear λ-Calculus (SS), pp. 151–165.
- ICFP-2006-WalkerMLRA #static typing #type system
- Static typing for a faulty λ calculus (DW, LWM, JL, GAR, DIA), pp. 38–49.
- FoSSaCS-2006-BlanquiKR #confluence #on the
- On the Confluence of λ-Calculus with Conditional Rewriting (FB, CK, CR), pp. 382–397.
- LICS-2006-Lassen #bisimulation #normalisation #μ-calculus
- Head Normal Form Bisimulation for Pairs and the λμ-Calculus (SBL), pp. 297–306.
- LICS-2006-ManzonettoS #algebra
- Boolean Algebras for λ Calculus (GM, AS), pp. 317–326.
- RTA-2005-Rocheteau #call-by #μ-calculus
- λμ-Calculus and Duality: Call-by-Name and Call-by-Value (JR), pp. 204–218.
- RTA-2005-Simpson #linear #reduction #semantics
- Reduction in a Linear λ-Calculus with Applications to Operational Semantics (AKS), pp. 219–234.
- RTA-2005-Yoshinaka #higher-order #linear
- Higher-Order Matching in the Linear λ Calculus in the Absence of Constants Is NP-Complete (RY), pp. 235–249.
- TLCA-2005-CoppolaLR #call-by #logic
- Elementary Affine Logic and the Call-by-Value λ Calculus (PC, UDL, SRDR), pp. 131–145.
- TLCA-2005-Coquand #theorem
- Completeness Theorems and λ-Calculus (TC), pp. 1–9.
- TLCA-2005-DavidN #normalisation #proving #symmetry #μ-calculus
- Arithmetical Proofs of Strong Normalization Results for the Symmetric λμ-Calculus (RD, KN), pp. 162–178.
- TLCA-2005-SelingerV #quantum
- A λ Calculus for Quantum Computation with Classical Control (PS, BV), pp. 354–368.
- TLCA-2005-SeveriV
- Continuity and Discontinuity in λ Calculus (PS, FJdV), pp. 369–385.
IFL-2005-Mackie #encoding #interactive- Encoding Strategies in the λ Calculus with Interaction Nets (IM), pp. 19–36.
QAPL-2004-HankinW05 #program analysis- λ-calculus and Quantitative Program Analysis: (CH, HW), pp. 5–18.
- LICS-2005-Saurin #μ-calculus
- Separation with Streams in the λμ-calculus (AS), pp. 356–365.
- ICALP-2004-Atkey
- A λ-Calculus for Resource Separation (RA), pp. 158–170.
- RTA-2004-Blom #approach #approximate
- An Approximation Based Approach to Infinitary λ Calculi (SB), pp. 221–232.
- POPL-2004-BalatCF #normalisation #partial evaluation
- Extensional normalisation and type-directed partial evaluation for typed λ calculus with sums (VB, RDC, MPF), pp. 64–76.
- FoSSaCS-2004-BaillotM #polynomial
- Soft λ-Calculus: A Language for Polynomial Time Computation (PB, VM), pp. 27–41.
- CSL-2004-Goubault-LarrecqLNZ #encryption #logic
- Complete Lax Logical Relations for Cryptographic λ-Calculi (JGL, SL, DN, YZ), pp. 400–414.
- CSL-2004-GrooteS #higher-order #linear
- Higher-Order Matching in the Linear λ-calculus with Pairing (PdG, SS), pp. 220–234.
- CSL-2004-Schroder #logic #similarity
- The Logic of the Partial λ-Calculus with Equality (LS), pp. 385–399.
- LICS-2004-BaillotT #polynomial
- Light Types for Polynomial Time Computation in λ-Calculus (PB, KT), pp. 266–275.
- LICS-2004-BucciarelliS #graph
- The Sensible Graph Theories of λ Calculus (AB, AS), pp. 276–285.
- LICS-2004-VIICHP #distributed #symmetry
- A Symmetric Modal λ Calculus for Distributed Computing (TMV, KC, RH, FP), pp. 286–295.
- RTA-2003-SalvatiG #complexity #higher-order #linear #on the
- On the Complexity of Higher-Order Matching in the Linear λ-Calculus (SS, PdG), pp. 234–245.
- TLCA-2003-Fujita #μ-calculus
- A Sound and Complete CPS-Translation for λμ-Calculus (KeF), pp. 120–134.
- CSL-2003-DavidG #normalisation
- Strong Normalization of the Typed λws-Calculus (RD, BG), pp. 155–168.
- RTA-2002-KennawayKP #composition #static analysis
- Static Analysis of Modularity of β-Reduction in the Hyperbalanced λ-Calculus (RK, ZK, AP), pp. 51–65.
- FLOPS-2002-DanvyS #polynomial
- λ-Lifting in Quadratic Time (OD, UPS), pp. 134–151.
- FLOPS-2002-Hasegawa #continuation #linear #monad
- Linearly Used Effects: Monadic and CPS Transformations into the Linear λ Calculus (MH), pp. 167–182.
- POPL-2002-RamseyP #monad #probability
- Stochastic λ calculus and monads of probability distributions (NR, AP), pp. 154–165.
- PPDP-2002-Fiore #analysis #evaluation #normalisation #semantics
- Semantic analysis of normalisation by evaluation for typed λ calculus (MPF), pp. 26–37.
- LICS-2002-FioreCB #morphism
- Remarks on Isomorphisms in Typed λ Calculi with Empty and Sum Types (MPF, RDC, VB), p. 147–?.
- RTA-2001-VestergaardB #confluence #first-order #proving #using
- A Formalised First-Order Confluence Proof for the λ-Calculus Using One-Sorted Variable Names (RV, JB), pp. 306–321.
- TLCA-2001-AltenkirchC #polymorphism
- A Finitary Subsystem of the Polymorphic λ-Calculus (TA, TC), pp. 22–28.
- TLCA-2001-Filinski #evaluation #normalisation
- Normalization by Evaluation for the Computational λ-Calculus (AF), pp. 151–165.
- TLCA-2001-Gianantonio #game studies #lazy evaluation #semantics
- Game Semantics for the Pure Lazy λ-calculus (PDG), pp. 106–120.
- TLCA-2001-Joly
- The Finitely Generated Types of the λ-Calculus (TJ), pp. 240–252.
- TLCA-2001-Matthes #higher-order #induction #μ-calculus
- Parigot’s Second Order λμ-Calculus and Inductive Types (RM), pp. 329–343.
- TLCA-2001-Pinto #geometry #implementation #interactive #modelling #parallel #using
- Parallel Implementation Models for the λ-Calculus Using the Geometry of Interaction (JSP), pp. 385–399.
- CSL-2001-AbramskyL #modelling
- Fully Complete Minimal PER Models for the Simply Typed λ-Calculus (SA, ML), pp. 443–457.
- CSL-2001-Akama #algebra #combinator #logic #towards
- Limiting Partial Combinatory Algebras towards Infinitary λ-Calculi and Classical Logic (YA), pp. 399–413.
- LICS-2001-AltenkirchDHS #evaluation #normalisation
- Normalization by Evaluation for Typed λ Calculus with Coproducts (TA, PD, MH, PJS), pp. 303–310.
- LICS-2001-Salibra #semantics
- A Continuum of Theories of λ Calculus without Semantics (AS), pp. 334–343.
- RTA-2000-JoachimskiM #confluence #standard
- Standardization and Confluence for a λ Calculus with Generalized Applications (FJ, RM), pp. 141–155.
- PPDP-2000-PediciniQ #implementation #parallel #reduction
- A parallel implementation for optimal λ-calculus reduction (MP, FQ), pp. 3–14.
- FoSSaCS-2000-HonsellLST #refinement
- Constructive Data Refinement in Typed λ Calculus (FH, JL, DS, AT), pp. 161–176.
- TLCA-1999-Fujita #call-by #morphism #polymorphism #μ-calculus
- Explicitly Typed λμ-Calculus for Polymorphism an Call-by-Value (KeF), pp. 162–176.
- TLCA-1999-GianantonioFH #game studies #semantics
- Game Semantics for Untyped λβη-Calculus (PDG, GF, FH), pp. 114–128.
- TLCA-1999-OHearn
- Resource Interpretations, Bunched Implications and the αλ-Calculus (PWO), pp. 258–279.
- FLOPS-1999-Danvy
- An Extensional Characterization of λ-Lifting and λ-Dropping (OD), pp. 241–250.
- PEPM-1999-Mogensen
- Gödelization in the Untyped λ-Calculus (TÆM), pp. 19–24.
CADE-1999-NadathurM #automaton #compilation #implementation #prolog- System Description: Teyjus — A Compiler and Abstract Machine Based Implementation of lambda-Prolog (GN, DJM), pp. 287–291.
- CSL-1999-FernandezM #reduction
- Closed Reductions in the λ-Calculus (MF, IM), pp. 220–234.
- CSL-1999-IshtiaqP #modelling
- Kripke Resource Models of a Dependently-Typed, Bunched λ-Calculus (SSI, DJP), pp. 235–249.
- LICS-1999-BanerjeeHR #analysis #polymorphism
- Region Analysis and the Polymorphic λ Calculus (AB, NH, JGR), pp. 88–97.
- ICFP-1998-KutznerS #call-by #nondeterminism
- A Non-Deterministic Call-by-Need λ Calculus (AK, MSS), pp. 324–335.
OOPSLA-1998-GianantonioHL #self- A λ Calculus of Objects with Self-Inflicted Extension (PDG, FH, LL), pp. 166–178.
- CADE-1998-Beeson #unification
- Unification in Lambda-Calculi with if-then-else (MB), pp. 103–118.
- ICALP-1997-CosmoG #composition #higher-order #on the
- On Modular Properties of Higher Order Extensional λ Calculi (RDC, NG), pp. 237–247.
- TLCA-1997-BonoB #constraints
- Matching Constraints for the λ Calculus of Objects (VB, MB), pp. 46–62.
- TLCA-1997-Hasegawa #category theory #modelling #recursion
- Recursion from Cyclic Sharing: Traced Monoidal Categories and Models of Cyclic λ Calculi (MH), pp. 196–213.
- TLCA-1997-Lenisa #induction #semantics
- Semantic Techniques for Deriving Coinductive Characterizations of Observational Equivalences for λ-calculi (ML), pp. 248–266.
- TLCA-1997-Urzyczyn #approach
- Inhabitation in Typed λ-Calculi (A Syntactic Approach) (PU), pp. 373–389.
- TLCA-1997-Xi #normalisation
- Weak and Strong β Normalisations in Typed λ-Calculi (HX), pp. 390–404.
- ALP-1997-BartheKR
- Explicit Substitutions for the λ-Calculus (GB, FK, AR), pp. 209–223.
- PEPM-1997-AsaiMY #call-by #partial evaluation
- Partial Evaluation of Call-by-Value λ-Calculus with Side-Effects (KA, HM, AY), pp. 12–21.
- PEPM-1997-DanvyS #equation #named #recursion #source code
- λ-Dropping: Transforming Recursive Equations into Programs with Block Structure (OD, UPS), pp. 90–106.
- PEPM-1997-NielsonN #framework #multi
- Prescriptive Frameworks for Multi-Level λ-Calculi (FN, HRN), pp. 193–202.
TAPSOFT-1997-Lenisa #induction #proving- A Uniform Syntactical Method for Proving Coinduction Principles in Lambda-Calculi (ML), pp. 309–320.
- CADE-1997-HutterK
- A Colored Version of the Lambda-Calculus (DH, MK), pp. 291–305.
- CSL-1997-Hofmann #linear #recursion
- A Mixed Modal/Linear λ Calculus with Applications to Bellantoni-Cook Safe Recursion (MH0), pp. 275–294.
- CSL-1997-Moschovakis #concurrent #game studies #recursion
- A Game-Theoretic, Concurrent and Fair Model of the Typed λ-calculus, with Full Recursion (YNM), pp. 341–359.
- LICS-1997-HofmannS #continuation #modelling #μ-calculus
- Continuation Models are Universal for λμ-Calculus (MH, TS), pp. 387–395.
- RTA-1996-FettigL #finite #higher-order #unification
- Unification of Higher-Order patterns in a Simply Typed λ-Calculus with Finite Products and terminal Type (RF, BL), pp. 347–361.
- RTA-1996-Kesner #confluence
- Confluence Properties of Extensional and Non-Extensional λ-Calculi with Explicit Substitutions (DK), pp. 184–199.
- ICFP-1996-LawallM #cost analysis #question #what
- Optimality and Inefficiency: What Isn’t a Cost Model of the λ Calculus? (JLL, HGM), pp. 92–101.
- ICFP-1996-LeeF #formal method #incremental #towards
- Enriching the λ Calculus with Contexts: Toward a Theory of Incremental Program Construction (SDL, DPF), pp. 239–250.
- ALP-1996-FerreiraKP #composition #normalisation
- λ-Calculi with Explicit Substitutions and Composition Which Preserve β-Strong Normalization (MCFF, DK, LP), pp. 284–298.
- CSL-1996-Roversi #resource management
- A Type-Free Resource-Aware λ-Calculus (LR), pp. 399–413.
- LICS-1996-BentonW #linear #logic #monad
- Linear Logic, Monads and the λ Calculus (PNB, PW), pp. 420–431.
- LICS-1996-HillebrandK #on the #power of
- On the Expressive Power of Simply Typed and Let-Polymorphic λ Calculi (GGH, PCK), pp. 253–263.
- RTA-1995-Asperti #exclamation #implementation #optimisation
- deltao!Epsilon = 1 — Optimizing Optimal λ-Calculus Implementations (AA), pp. 102–116.
- RTA-1995-KennawayKSV #modelling
- Infinitary λ Calculi and Böhm Models (RK, JWK, MRS, FJdV), pp. 257–270.
- TLCA-1995-AspertiL #graph
- Comparing λ-calculus translations in Sharing Graphs (AA, CL), pp. 1–15.
- TLCA-1995-Dowek #combinator #comprehension
- λ-calculus, Combinators and the Comprehension Scheme (GD), pp. 154–170.
- TLCA-1995-Holmes #type system
- Untyped λ-Calculus with Relative Typing (MRH), pp. 235–248.
- TLCA-1995-HonsellL #semantics
- Final Semantics for untyped λ-calculus (FH, ML), pp. 249–265.
- TLCA-1995-Mellie
- Typed λ-calculi with explicit substitutions may not terminate (PAM), pp. 328–334.
- TLCA-1995-PravatoRR #call-by #category theory #semantics
- Categorical semantics of the call-by-value λ-calculus (AP, SRDR, LR), pp. 381–396.
- TLCA-1995-RitterP #ml #standard
- A Fully Abstract Translation between a λ-Calculus with Reference Types and Standard ML (ER, AMP), pp. 397–413.
- TLCA-1995-Simpson #category theory
- Categorical completeness results for the simply-typed λ-calculus (AKS), pp. 414–427.
- PEPM-1995-Mogensen #online #partial evaluation #self
- Self-applicable Online Partial Evaluation of Pure λ Calculus (TÆM), pp. 39–44.
- PLILP-1995-KamareddineR
- A λ-calculus à la de Bruijn with Explicit Substitutions (FK, AR), pp. 45–62.
- POPL-1995-AriolaFMOW #call-by
- The Call-by-Need λ Calculus (ZMA, MF, JM, MO, PW), pp. 233–246.
SAS-1995-PalsbergO #trust- Trust in the λ-Calculus (JP, PØ), pp. 314–329.
- LICS-1995-AbramskyM #abstraction #game studies #lazy evaluation
- Games and Full Abstraction for the Lazy λ-Calculus (SA, GM), pp. 234–243.
- LICS-1995-KfouryW #normalisation #proving #reduction #semantics
- New Notions of Reduction and Non-Semantic Proofs of β-Strong Normalization in Typed λ-Calculi (AJK, JBW), pp. 311–321.
PODS-1994-HillebrandK #database #functional #order #query- Functional Database Query Languages as Typed Lambda Calculi of Fixed Order (GGH, PCK), pp. 222–231.
- ICALP-1994-CosmoK #algebra #first-order #recursion #term rewriting
- Combining First Order Algebraic Rewriting Systems, Recursion and Extensional λ Calculi (RDC, DK), pp. 462–472.
LFP-1994-KfouryW #algorithm #higher-order #type inference- A Direct Algorithm for Type Inference in the Rank-2 Fragment of the Second-Order λ-Calculus (AJK, JBW), pp. 196–207.
- PEPM-1994-CourtenageC #type inference
- Analysing Resource Use in the λ Calculus by Type Inference (SC, CDC), pp. 33–41.
- POPL-1994-Bloom #communication #higher-order #named
- CHOCOLATE: Calculi of Higher Order COmmunication and LAmbda TErms (BB), pp. 339–347.
- POPL-1994-GarrigueA #polymorphism
- The Typed Polymorphic Label-Selective λ-Calculus (JG, HAK), pp. 35–47.
- POPL-1994-TofteT #call-by #implementation #stack #using
- Implementation of the Typed Call-by-Value λ-Calculus using a Stack of Regions (MT, JPT), pp. 188–201.
- SAS-1994-BanerjeeS #call-by
- Stackability in the Simply-Typed Call-by-Value λ Calculus (AB, DAS), pp. 131–146.
- ESOP-1994-Boerio #higher-order #polymorphism
- Extending Pruning Techniques to Polymorphic Second order λ-Calculus (LB), pp. 120–134.
- CADE-1994-JohannK #constant #order #unification
- Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading (PJ, MK), pp. 620–634.
- LICS-1994-AspertiDLR
- Paths in the λ-calculus (AA, VD, CL, LR), pp. 426–436.
- LICS-1994-Wells #decidability #higher-order
- Typability and Type-Checking in the Second-Order λ-Calculus are Equivalent and Undecidable (JBW), pp. 176–185.
- ICALP-1993-CosmoK #confluence #recursion #reduction
- A Confluent Reduction for the Extensional Typed λ-Calculus with Pairs, Sums, Recursion and terminal Object (RDC, DK), pp. 645–656.
- RTA-1993-AspertiL
- Paths, Computations and Labels in the λ-Calculus (AA, CL), pp. 152–167.
- RTA-1993-Dougherty
- Some λ Calculi with Categorial Sums and Products (DJD), pp. 137–151.
- TLCA-1993-Jacobs #semantics
- Semantics of λ-I and of other substructure λ calculi (BJ0), pp. 195–208.
- TLCA-1993-LeivantM
- λ calculus characterizations of poly-time (DL, JYM), pp. 274–288.
- TLCA-1993-Takahashi
- λ-Calculi with Conditional Rules (MT), pp. 406–417.
FPCA-1993-Yoshida #reduction- Optimal Reduction in Weak-λ-calculus with Shared Environments (NY), pp. 243–254.
- POPL-1993-OderskyRH #call-by
- Call by Name, Assignment, and the λ Calculus (MO, DR, PH), pp. 43–56.
- CSL-1993-Ritter #normalisation
- Normalization for Typed λ Calculi with Explicit Substitution (ER), pp. 295–304.
- ILPS-1993-KohlhaseP #unification
- Unification in a λ-Calculus with Intersection Types (MK, FP), pp. 488–505.
- ICALP-1992-Ong #lazy evaluation #modelling
- Lazy λ Calculus: Theories, Models and Local Structure Characterization (CHLO), pp. 487–498.
- ALP-1992-LaneveM #axiom #equivalence #permutation
- Axiomatizing Permutation Equivalence in the λ-Calculus (CL, UM), pp. 350–363.
- PEPM-1992-Mogensen #partial evaluation #self
- Self-applicable Partial Evaluation for Pure λ Calculus (TÆM), pp. 116–121.
- CADE-1992-NipkowQ #reduction #type system #unification
- Reduction and Unification in Lambda Calculi with Subtypes (TN, ZQ), pp. 66–78.
- CSL-1992-BentonBPH #linear #modelling #revisited
- Linear λ-Calculus and Categorial Models Revisited (PNB, GMB, VdP, MH), pp. 61–84.
- CSL-1992-BerarducciB #normalisation #self
- A Self-Interpreter of λ Calculus Having a Normal Form (AB, CB), pp. 85–99.
- LICS-1992-Geuvers
- The Church-Rosser Property for βη-reduction in Typed λ-Calculi (HG), pp. 453–460.
- LICS-1992-LiguoroPS
- Retracts in simply typed λβη-calculus (Ud, AP, RS), pp. 461–469.
- LICS-1992-LincolnM #aspect-oriented #linear
- Operational aspects of linear λ calculus (PL, JCM), pp. 235–246.
- LICS-1992-Sangiorgi #concurrent #lazy evaluation
- The Lazy λ Calculus in a Concurrency Scenario (DS), pp. 102–109.
- ICALP-1991-CurienC #reduction
- A Concluent Reduction for the λ-Calculus with Surjective Pairing and Terminal Object (PLC, RDC), pp. 291–302.
- RTA-1991-Dougherty #algebra
- Adding Algebraic Rewriting to the Untyped λ Calculus (DJD), pp. 37–48.
- FPCA-1991-FrandsenS #implementation #performance #question #what
- What is an Efficient Implementation of the λ-calculus? (GSF, CS), pp. 289–312.
- PEPM-1991-MichaylovP #compilation #polymorphism
- Compiling the Polymorphic λ-Calculus (SM, FP), pp. 285–296.
- POPL-1991-CrankF
- Parameter-Passing and the λ Calculus (EC, MF), pp. 233–244.
- POPL-1991-HengleinM #complexity #higher-order #type inference
- The Complexity of Type Inference for Higher-Order Typed λ Calculi (FH, HGM), pp. 119–130.
- POPL-1991-Maranget #orthogonal #term rewriting
- Optimal Derivations in Weak λ-calculi and in Orthogonal Terms Rewriting Systems (LM), pp. 255–269.
- LICS-1991-BergerS #evaluation #functional
- An Inverse of the Evaluation Functional for Typed λ-calculus (UB, HS), pp. 203–211.
- LICS-1991-MalacariaR #algebra
- Some Results on the Interpretation of λ-calculus in Operator Algebras (PM, LR), pp. 63–72.
- LICS-1991-Tronci #equation
- Equational Prgoramming in λ-calculus (ET), pp. 191–202.
- LFP-1990-FieldT #incremental #reduction
- Incremental Reduction in the λ Calculus (JF, TT), pp. 307–322.
- POPL-1990-Lamping #algorithm #reduction
- An Algorithm for Optimal λ Calculus Reduction (JL), pp. 16–30.
- ESOP-1990-BarendregtH #programming language
- Types in λ Calculi and Programming Languages (HB, KH), pp. 1–35.
- CADE-1990-FeltyGMP #prolog #tutorial
- Tutorial on Lambda-Prolog (APF, ELG, DM, FP), p. 682.
- CADE-1990-FeltyM #encoding #logic programming #programming language
- Encoding a Dependent-Type Lambda-Calculus in a Logic Programming Language (APF, DM), pp. 221–235.
- LICS-1990-GuzmanH #polymorphism #thread
- Single-Threaded Polymorphic λ Calculus (JCG, PH), pp. 333–343.
- LICS-1990-KfouryT #polymorphism #re-engineering
- Type Reconstruction in Finite-Rank Fragments of the Polymorphic λ-Calculus (AJK, JT), pp. 2–11.
- CAAP-1989-Boudol #communication #concurrent #towards
- Towards a Lambda-Calculus for Concurrent and Communicating Systems (GB), pp. 149–161.
- CCIPL-1989-FradetM #compilation #functional
- Compilation of Lambda-Calculus into Functional Machine Code (PF, DLM), pp. 155–166.
- CSL-1989-Parigot #on the #representation
- On the Representation of Data in λ-Calculus (MP), pp. 309–321.
- LICS-1989-Moggi #monad
- Computational λ-Calculus and Monads (EM), pp. 14–23.
- LICS-1989-Vrijer
- Extending the λ Calculus with Surjective Pairing is Conservative (RCdV), pp. 204–215.
VDME-1988-BorzyszkowskiKS #formal method #polymorphism- A Set-Theoretic Model for a Typed Polymorphic λ Calculus — A Contribution to MetaSoft (AMB, RK, SS), pp. 267–298.
- LFP-1988-Felleisen #named
- λ-V-CS: An Extended λ-Calculus for Scheme (MF), pp. 72–85.
- POPL-1988-NielsonN #analysis #automation
- Automatic Binding Time Analysis for a Typed λ-Calculus (HRN, FN), pp. 98–106.
- ESOP-1988-NielsonN
- 2-level λ-lifting (FN, HRN), pp. 328–343.
- CADE-1988-FeltyGHMNS #logic programming #named #programming language #prolog
- Lambda-Prolog: An Extended Logic Programming Language (APF, ELG, JH, DM, GN, AS), pp. 754–755.
- LICS-1988-Amadio #fixpoint #higher-order #modelling
- A fixed point extension of the second order λ-calculus: observable equivalences and models (RMA), pp. 51–60.
- LICS-1988-Bloom #modelling
- Can LCF Be Topped? Flat Lattice models of Typed λ Calculus (BB), pp. 282–295.
- LICS-1988-FreydGSS #parametricity #polymorphism #semantics
- Semantic Parametricity in Polymorphic λ Calculus (PJF, JYG, AS, PJS), pp. 274–279.
- POPL-1987-MeyerMMS #polymorphism
- Empty Types in Polymorphic λ Calculus (ARM, JCM, EM, RS), pp. 253–262.
- LICS-1987-BohmT
- X-Separability and Left-Invertibility in λ-calculus (CB, ET), pp. 320–328.
- LICS-1987-FreydS #aspect-oriented #polymorphism #semantics
- Some Semantic Aspects of Polymorphic λ Calculus (PJF, AS), pp. 315–319.
- LICS-1987-Mendler #constraints #higher-order #recursion
- Recursive Types and Type Constraints in Second-Order λ Calculus (NPM), pp. 30–36.
- LICS-1987-MitchellM #modelling
- Kripke-Style models for typed λ calculus (JCM, EM), pp. 303–314.
- POPL-1986-HudakY #analysis #higher-order #strict
- Higher-Order Strictness Analysis in Untyped λ Calculus (PH, JY), pp. 97–109.
- LICS-1986-AmadioBL #equation #higher-order
- The Finitary Projection Model for Second Order λ Calculus and Solutions to Higher Order Domain Equations (RMA, KBB, GL), pp. 122–130.
- RTA-1985-Zaionc #regular expression #set
- The Set of Unifiers in Typed λ-Calculus as Regular Expression (MZ), pp. 430–440.
- CAAP-1985-Karr #proving
- “Delayability” in Proofs of Strong Normalizability in the Typed Lambda Calculus (MK), pp. 208–222.
- ICALP-1982-BerklingF #functional #programming language
- A Modification of the λ-Calculus as a Base for Functional Programming Languages (KJB, EF), pp. 35–47.
SDCG-1980-Schmidt - State transition machines for λ calculus expressions (DAS), pp. 415–440.
- CADE-1980-Nederpelt #approach #proving #theorem proving
- An Approach to Theorem Proving on the Basis of a Typed Lambda-Calculus (RN), pp. 182–194.
- ICALP-1979-CoppoDS #functional #semantics
- Functional Characterization of Some Semantic Equalities inside λ-Calculus (MC, MDC, PS), pp. 133–146.
- ICALP-1978-Berry #modelling
- Stable Models of Typed λ-Calculi (GB), pp. 72–89.
- ICALP-1978-CoppoDR #finite #set
- (Semi)-separability of Finite Sets of Terms in Scott’s D∞-Models of the λ-Calculus (MC, MDC, SRDR), pp. 142–164.
- ICALP-1978-Sale #french
- Une Extension de la Theorie des Types en λ-Calcul (PS), pp. 398–410.
GG-1978-Staples #reduction- A Graph-Like λ Calculus for Which Leftmost-Overmost Reduction is Optimal (JS), pp. 440–455.
- ICALP-1977-BohmCD #termination #testing
- Termination Tests inside λ-Calculus (CB, MC, MDC), pp. 95–110.
