BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
λ-calculus
Google λ-calculus
Wikidata Q242028
WikipediaGerman Lambda-Kalkül
WikipediaEnglish Lambda calculus
WikipediaFrench Lambda-calcul
WikipediaRussian Лямбда-исчисление

Tag #λ-calculus

283 papers:

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

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.