BibSLEIGH — type system tag

type system

type system

Tag #type system

663 papers:

POPL-2020-ChangBTB #dependent type #metaprogramming: Dependent type systems as macros (SC, MB, MT, WJB), p. 29.
POPL-2020-MackayPAG #decidability #dependent type: Decidable subtyping for path dependent types (JM, AP, JA, LG), p. 27.
CSL-2020-Cavallo0 #parametricity: Internal Parametricity for Cubical Type Theory (EC, RH0), p. 17.
CSL-2020-CavalloMS #modelling: Unifying Cubical Models of Univalent Type Theory (EC, AM, AWS), p. 17.
FSCD-2019-BlanquiGH #dependence #dependent type #modulo theories #termination: Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting (FB, GG, OH), p. 21.
FSCD-2019-CoquandHS: Homotopy Canonicity for Cubical Type Theory (TC, SH, CS), p. 23.
FSCD-2019-KaposiHS: Gluing for Type Theory (AK, SH, CS), p. 19.
ICFP-2019-GratzerSB #dependent type #implementation: Implementing a modal dependent type theory (DG, JS, LB), p. 29.
ICFP-2019-PedrotTFT: A reasonably exceptional type theory (PMP, NT, HJF, ÉT), p. 29.
ECOOP-2019-ChungNV #algorithm #performance #tuple: Julia's Efficient Algorithm for Subtyping Unions and Covariant Tuples (Pearl) (BC, FZN, JV), p. 15.
ECOOP-2019-MisonizhnikM #on the #satisfiability: On Satisfiability of Nominal Subtyping with Variance (AM, DM), p. 20.
ECOOP-2019-Muijnck-HughesV #hardware #interface: A Typing Discipline for Hardware Interfaces (JdMH, WV), p. 27.
ECOOP-2019-PelsmaekerAV #declarative #editing #idea #parametricity #semantics #specification #towards: Towards Language-Parametric Semantic Editor Services Based on Declarative Type System Specifications (Brave New Idea Paper) (DAAP, HvA, EV), p. 18.
OOPSLA-2019-NearDASGWSZSSS #difference #higher-order #linear #named #privacy: Duet: an expressive higher-order language and linear type system for statically enforcing differential privacy (JPN, DD, CA, TS, PG, LW, NS, MZ0, NS, AS, DS), p. 30.
OOPSLA-2019-WangHZTT #named #performance #polymorphism: IVT: an efficient method for sharing subtype polymorphic objects (YPW, XQH, ZXZ, WT, GT), p. 22.
PLDI-2019-KuhlenschmidtAS #performance #towards: Toward efficient gradual typing for structural types via coercions (AK, DA, JGS), pp. 517–532.
POPL-2019-CastagnaLPS #perspective: Gradual typing: a new perspective (GC, VL, TP, JGS), p. 32.
POPL-2019-CavalloH #induction: Higher inductive types in cubical computational type theory (EC, RH0), p. 27.
POPL-2019-MiyazakiSI #type inference: Dynamic type inference for gradual Hindley-Milner typing (YM0, TS, AI), p. 29.
POPL-2019-NewLA: Gradual type theory (MSN, DRL, AA), p. 31.
ESEC-FSE-2019-BanerjeeCS #java #named #null #safety: NullAway: practical type-based null safety for Java (SB, LC, MS), pp. 740–750.
ESOP-2019-Gilbert: Verifiable Certificates for Predicate Subtyping (FG0), pp. 440–466.
ICTSS-2019-AragaoASCLD #named #process: TestDCat: Catalog of Test Debt Subtypes and Management Activities (BSA, RMCA, ISS, RNSC, VL, TGRD), pp. 279–295.
FSCD-2018-LicataOPS #modelling: Internal Universes in Models of Homotopy Type Theory (DRL, IO, AMP, BS), p. 17.
FSCD-2018-MannaaM #semantics: The Clocks They Are Adjunctions Denotational Semantics for Clocked Type Theory (BM, REM), p. 17.
FSCD-2018-NewL #call-by: Call-by-Name Gradual Type Theory (MSN, DRL), p. 17.
ICFP-2018-Campora0W #performance #safety: Casts and costs: harmonizing safety and performance in gradual typing (JPCI, SC0, EW), p. 30.
CIKM-2018-XuLHLXYW #corpus #multi #named: METIC: Multi-Instance Entity Typing from Corpus (BX, ZL, LH, BL, YX, DY, WW0), pp. 903–912.
ECOOP-2018-ChungLNV #named: KafKa: Gradual Typing for Objects (BC, PL, FZN, JV), p. 24.
ECOOP-2018-OostvogelsKM #constraints #interface #static typing: Static Typing of Complex Presence Constraints in Interfaces (NO, JDK, WDM), p. 27.
OOPSLA-2018-FelteyGSFS #contract: Collapsible contracts: fixing a pathology of gradual typing (DF, BG, CS, RBF, VSA), p. 27.
OOPSLA-2018-MuehlboeckT: Empowering union and intersection types with integrated subtyping (FM, RT), p. 29.
OOPSLA-2018-NardelliBPCBV #re-engineering: Julia subtyping: a rational reconstruction (FZN, JB, AP, BC, JB, JV), p. 27.
POPL-2018-0001OV #decidability: Decidability of conversion for type theory in type theory (AA0, JÖ, AV), p. 29.
POPL-2018-0001ST #higher-order #nondeterminism #refinement #source code #verification: Relatively complete refinement type system for verification of higher-order non-deterministic programs (HU0, YS, TT), p. 29.
POPL-2018-ChandraB #named #reasoning: Bonsai: synthesis-based reasoning for type systems (KC, RB), p. 34.
ICSE-2018-LaraG #analysis #concept #modelling: A posteriori typing for model-driven engineering: concepts, analysis, and applications (JdL, EG), p. 1136.
ICSE-2018-RadhakrishnaLMM #android #named: DroidStar: callback typestates for Android classes (AR, NVL, SM, SM, KCS, DZ, BYEC, PC), pp. 1160–1170.
SLE-2018-RacordonB #alias: A practical type system for safe aliasing (DR, DB), pp. 133–146.
ESOP-2018-PedrotT: Failure is Not an Option - An Exceptional Type Theory (PMP, NT), pp. 245–271.
ESOP-2018-SalehKPS: Explicit Effect Subtyping (AHS, GK, MP, TS), pp. 327–354.
ESOP-2018-VieringCEHZ #distributed: A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems (MV, TCC, PE, RH, LZ), pp. 799–826.
ESOP-2018-XieBO #consistency: Consistent Subtyping for All (NX, XB, BCdSO), pp. 3–30.
CSL-2018-AngiuliF0 #reasoning: Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities (CA, KBH(, RH0), p. 17.
ICPC-2017-MilojkovicGN17a #exclamation: It's duck (typing) season! (NM, MG, ON), pp. 312–315.
FSCD-2017-Gaboardi #higher-order #relational #source code #verification: Type Systems for the Relational Verification of Higher Order Programs (Invited Talk) (MG), p. 1.
FSCD-2017-OrtonP #modelling: Models of Type Theory Based on Moore Paths (IO, AMP), p. 16.
ICFP-2017-CastagnaL: Gradual typing with union and intersection types (GC, VL), p. 28.
ICFP-2017-CosmanJ #refinement: Local refinement typing (BC, RJ), p. 27.
ICFP-2017-IgarashiSI #on the #polymorphism: On polymorphic gradual typing (YI, TS, AI), p. 29.
ICFP-2017-NuytsVD #dependent type #parametricity #quantifier: Parametric quantifiers for dependent type theory (AN, AV, DD), p. 29.
KDD-2017-BaytasXZWJZ #network: Patient Subtyping via Time-Aware LSTM Networks (IMB, CX, XZ, FW0, AKJ0, JZ), pp. 65–74.
KDD-2017-CaoZZYPZARL #detection #mobile #modelling #named: DeepMood: Modeling Mobile Phone Typing Dynamics for Mood Detection (BC, LZ, CZ, PSY, AP, JZ, OA, KR, ADL), pp. 747–755.
ECOOP-2017-Tate: Retargeting Gradual Typing (Invited Talk) (RT), p. 1.
OOPSLA-2017-BaumanBST: Sound gradual typing: only mostly dead (SB, CFBT, JGS, STH), p. 24.
OOPSLA-2017-ClebschFDYWV #co-evolution #design #garbage collection #named: Orca: GC and type system co-design for actor languages (SC, JF, SD, AMY, TW, JV), p. 28.
OOPSLA-2017-MuehlboeckT: Sound gradual typing is nominally alive and well (FM, RT), p. 30.
OOPSLA-2017-RichardsAT #virtual machine: The VM already knew that: leveraging compile-time knowledge to optimize gradual typing (GR, EA, AT), p. 27.
OOPSLA-2017-YangO: Unifying typing and subtyping (YY, BCdSO), p. 26.
PEPM-2017-FritzH #approximate #precise #python: Cost versus precision for approximate typing for Python (LF, JH), pp. 89–98.
POPL-2017-AngiuliHW: Computational higher-dimensional type theory (CA, RH0, TW), pp. 680–693.
POPL-2017-ChangKG #metaprogramming: Type systems as macros (SC, AK, BG), pp. 694–705.
POPL-2017-DolanM #morphism #polymorphism #type inference: Polymorphism, subtyping, and type inference in MLsub (SD, AM), pp. 60–72.
POPL-2017-VitousekSS #collaboration #runtime: Big types in little runtime: open-world soundness and collaborative blame for gradual type systems (MMV, CS, JGS), pp. 762–774.
SLE-2017-Boronat #constraints #ocl: Structural model subtyping with OCL constraints (AB), pp. 194–205.
ESOP-2017-LagoG #monad #probability #termination: Probabilistic Termination by Monadic Affine Sized Typing (UDL, CG), pp. 393–419.
FASE-2017-LaraRRGIPC #model transformation #modelling #requirements #reuse: Reusing Model Transformations Through Typing Requirements Models (JdL, JDR, DDR, EG, LI, AP, JSC), pp. 264–282.
CSL-2017-AhrensLV #category theory: Categorical Structures for Type Theory in Univalent Foundations (BA, PLL, VV), p. 16.
CSL-2017-EscardoK #recursion: Partial Elements and Recursion via Dominances in Univalent Type Theory (MHE, CMK), p. 16.
FSCD-2016-CoquandM #independence #markov: The Independence of Markov's Principle in Type Theory (TC, BM), p. 18.
FSCD-2016-Huet #deduction #education #formal method #functional #programming: Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization (GPH), p. 2.
Haskell-2016-PloegCB #dynamic typing #monad #type safety: The Key monad: type-safe unconstrained dynamic typing (AvdP, KC, PB), pp. 146–157.
ICFP-2016-CicekP0 #complexity #control flow #incremental: A type theory for incremental computational complexity with control flow changes (EÇ, ZP, DG0), pp. 132–145.
ICFP-2016-Licata #functional: A functional programmer's guide to homotopy type theory (DL), p. 3.
CIKM-2016-HanadaPCL #effectiveness #fault #using: Effective Spelling Correction for Eye-based Typing using domain-specific Information about Error Distribution (RH, MdGCP, MC, FAL), pp. 1723–1732.
KDD-2016-RenHQVJH #reduction: Label Noise Reduction in Entity Typing by Heterogeneous Partial-Label Embedding (XR, WH, MQ, CRV, HJ, JH0), pp. 1825–1834.
ECOOP-2016-AndreasenGCSTS #approach: Trace Typing: An Approach for Evaluating Retrofitted Type Systems (EA, CSG, SC0, MS, FT, KS), p. 26.
OOPSLA-2016-AminT #java #null #pointer #scala: Java and scala's type systems are unsound: the existential crisis of null pointers (NA, RT), pp. 838–848.
OOPSLA-2016-AnconaC #imperative #object-oriented #semantics: Semantic subtyping for imperative object-oriented languages (DA, AC), pp. 568–587.
PLDI-2016-KentKT #modulo theories: Occurrence typing modulo theories (AMK, DK0, STH), pp. 296–309.
POPL-2016-AltenkirchK #induction #using: Type theory in type theory using quotient inductive types (TA, AK), pp. 18–29.
POPL-2016-CiminiS #algorithm #generative: The gradualizer: a methodology and algorithm for generating gradual type systems (MC, JGS), pp. 443–455.
POPL-2016-GarciaCT: Abstracting gradual typing (RG, AMC, ÉT), pp. 429–442.
POPL-2016-TakikawaFGNVF #question: Is sound gradual typing dead? (AT, DF, BG, MSN, JV, MF), pp. 456–468.
FSE-2016-Santino #array: Enforcing correct array indexes with a type system (JS), pp. 1142–1144.
CSL-2016-AltenkirchCK #similarity #strict: Extending Homotopy Type Theory with Strict Equality (TA, PC, NK), p. 17.
CSL-2016-BirkedalBCGSV #recursion #similarity: Guarded Cubical Type Theory: Path Equality for Guarded Recursion (LB, AB, RC, HBG, BS, AV), p. 17.
CSL-2016-FavoniaS #theorem: The Seifert-van Kampen Theorem in Homotopy Type Theory (KBH(, MS), p. 16.
CSL-2016-OrtonP #axiom #modelling: Axioms for Modelling Cubical Type Theory in a Topos (IO, AMP), p. 19.
IJCAR-2016-SelsamM #congruence: Congruence Closure in Intensional Type Theory (DS, LdM), pp. 99–115.
HOFM-2015-ErbaturH #guidelines #named #programming: GuideForce: Type-Based Enforcement of Programming Guidelines (SE, MH0), pp. 75–89.
TLCA-2015-AhrensCS: Non-Wellfounded Trees in Homotopy Type Theory (BA, PC, RS), pp. 17–30.
TLCA-2015-BiernackiP #logic: Logical Relations for Coherence of Effect Subtyping (DB, PP), pp. 107–122.
TLCA-2015-HirschowitzHT: Wild ω-Categories for the Homotopy Hypothesis in Type Theory (AH, TH, NT), pp. 226–240.
TLCA-2015-WangC #independence: A Proof-theoretic Characterization of Independence in Type Theory (YW, KC), pp. 332–346.
ICFP-2015-BuirasVR #data flow #dynamic typing #haskell #named: HLIO: mixing static and dynamic typing for information-flow control in Haskell (PB, DV, AR), pp. 289–301.
ICFP-2015-GenevesG #problem #static typing #xquery: XQuery and static typing: tackling the problem of backward axes (PG, NG), pp. 88–100.
CHI-2015-FowlerPCBOZ #modelling #performance #personalisation: Effects of Language Modeling and its Personalization on Touchscreen Typing Performance (AF, KP, CC, XB, TO, SZ), pp. 649–658.
CHI-2015-SmithBZ #gesture #optimisation: Optimizing Touchscreen Keyboards for Gesture Typing (BAS, XB, SZ), pp. 3365–3374.
HCI-IT-2015-MeleMR #communication #predict #user interface: Beyond Direct Gaze Typing: A Predictive Graphic User Interface for Writing and Communicating by Gaze (MLM, DM, CER), pp. 66–77.
KDD-2015-RenEWH #approach #automation #corpus #mining #network #recognition: Automatic Entity Recognition and Typing from Massive Text Corpora: A Phrase and Network Mining Approach (XR, AEK, CW, JH), pp. 2319–2320.
KDD-2015-RenEWTVH #clustering #effectiveness #named #recognition: ClusType: Effective Entity Recognition and Typing by Relation Phrase-Based Clustering (XR, AEK, CW, FT, CRV, JH), pp. 995–1004.
MoDELS-2015-LaraGC #modelling: A-posteriori typing for Model-Driven Engineering (JdL, EG, JSC), pp. 156–165.
ECOOP-2015-JonesHN: Brand Objects for Nominal Typing (TJ, MH, JN), pp. 198–221.
ECOOP-2015-TakikawaFDFFTF #towards: Towards Practical Gradual Typing (AT, DF, ED, MF, RBF, STH, MF), pp. 4–27.
ECOOP-2015-VekrisCJ #trust #verification: Trust, but Verify: Two-Phase Typing for Dynamic Languages (PV, BC, RJ), pp. 52–75.
Onward-2015-GreweEWM #performance #proving: Type systems for the masses: deriving soundness proofs and efficient checkers (SG, SE, PW, MM), pp. 137–150.
PEPM-2015-KootH #analysis #exception #functional #higher-order #semantics #strict: Type-based Exception Analysis for Non-strict Higher-order Functional Languages with Imprecise Exception Semantics (RK, JH), pp. 127–138.
POPL-2015-RastogiSFBV #performance #typescript: Safe & Efficient Gradual Typing for TypeScript (AR, NS, CF, GMB, PV), pp. 167–180.
SAS-2015-ChoiCNS #javascript #layout #named: SJS: A Type System for JavaScript with Fixed Object Layout (WC, SC, GCN, KS), pp. 181–198.
ESOP-2015-Chugh #named #recursion #self: IsoLATE: A Type System for Self-recursion (RC), pp. 257–282.
ESOP-2015-FetscherCPHF #automation #generative #random: Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System (BF, KC, MHP, JH, RBF), pp. 383–405.
ESOP-2015-SiekVCTG #performance: Monotonic References for Efficient Gradual Typing (JGS, MMV, MC, STH, RG), pp. 432–456.
ESOP-2015-VasconcelosJFH #analysis #functional #lazy evaluation #recursion: Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages (PBV, SJ, MF, KH), pp. 787–811.
FoSSaCS-2015-SalvatiW: Typing Weak MSOL Properties (SS, IW), pp. 343–357.
ITiCSE-2014-Tirronen #case study #concept: Study on difficulties and misconceptions with modern type systems (VT), pp. 303–308.
ICPC-2014-PetersenHR #api #comparison #eclipse #empirical #groovy #ide #java: An empirical comparison of static and dynamic type systems on API usage in the presence of an IDE: Java vs. groovy with eclipse (PP, SH, RR), pp. 212–222.
CIAA-2014-DemailleDLSS #automaton: A Type System for Weighted Automata and Rational Expressions (AD, ADL, SL, LS, JS), pp. 162–175.
RTA-TLCA-2014-BizjakBM #nondeterminism: A Model of Countable Nondeterminism in Guarded Type Theory (AB, LB, MM), pp. 108–123.
RTA-TLCA-2014-Dezani-CiancagliniG #precise: Preciseness of Subtyping on Intersection and Union Types (MDC, SG), pp. 194–207.
RTA-TLCA-2014-EscardoS #data type: Abstract Datatypes for Real Numbers in Type Theory (MHE, AS), pp. 208–223.
RTA-TLCA-2014-RouxD: The Structural Theory of Pure Type Systems (CR, FvD), pp. 364–378.
FLOPS-2014-HoffmannS #analysis #array #integer: Type-Based Amortized Resource Analysis with Integers and Arrays (JH, ZS), pp. 152–168.
FLOPS-2014-NaR #formal method #subclass: A New Formalization of Subtyping to Match Subclasses to Subtypes (HN, SR), pp. 238–252.
ICFP-2014-ChenE #analysis #parametricity #product line: Type-based parametric analysis of program families (SC, ME), pp. 39–51.
IFL-2014-DomoszlaiLP #editing #named: Editlets: type-based, client-side editors for iTasks (LD, BL, RP), p. 6.
CHI-2014-BurgbacherH #gesture #verification: An implicit author verification system for text messages based on gesture typing biometrics (UB, KHH), pp. 2951–2954.
ICPR-2014-TaxSRM #performance: The Effect of Aggregating Subtype Performances Depends Strongly on the Performance Measure Used (DMJT, HMJS, MJTR, PDM), pp. 3720–3725.
ECOOP-2014-AnconaC #induction #object-oriented: Sound and Complete Subtyping between Coinductive Types for Object-Oriented Languages (DA, AC), pp. 282–307.
ECOOP-2014-MillerHO #concurrent #named: Spores: A Type-Based Foundation for Closures in the Age of Concurrency and Distribution (HM, PH, MO), pp. 308–333.
OOPSLA-2014-AllendeFGT: Confined gradual typing (EA, JF, RG, ÉT), pp. 251–270.
PLDI-2014-AhnCSGT #javascript #performance: Improving JavaScript performance by deconstructing the type system (WA, JC, TS, MJG, JT), p. 51.
POPL-2014-AtkeyGJ #dependent type #parametricity: A relationally parametric model of dependent type theory (RA, NG, PJ), pp. 503–516.
POPL-2014-ChenE #debugging #fault: Counter-factual typing for debugging type errors (SC, ME), pp. 583–594.
POPL-2014-SwamyFRBCSB #embedded #javascript: Gradual typing embedded securely in JavaScript (NS, CF, AR, KB, JC, PYS, GMB), pp. 425–438.
PPDP-2014-ChenDY #on the #precise: On the Preciseness of Subtyping in Session Types (TCC, MDC, NY), pp. 135–146.
ICSE-2014-EndrikatHRS #api #documentation #how #question #static typing #usability: How do API documentation and static typing affect API usability? (SE, SH, RR, AS), pp. 632–642.
ESOP-2014-ThiemannF: Gradual Typing for Annotated Type Systems (PT, LF), pp. 47–66.
FASE-2014-HuangDM #analysis #java #web: Type-Based Taint Analysis for Java Web Applications (WH, YD, AM), pp. 140–154.
ISSTA-2014-WeitzKSE #string: A type system for format strings (KW, GK, SS, MDE), pp. 127–137.
ISSTA-2014-XiaoBIMGC #analysis #dependence #effectiveness: ARC++: effective typestate and lifetime dependency analysis (XX, GB, FI, NM, AG, DC), pp. 116–126.
LICS-CSL-2014-LicataF: Eilenberg-MacLane spaces in homotopy type theory (DRL, EF), p. 9.
LICS-CSL-2014-Mogelberg #effectiveness #recursion: A type theory for productive coprogramming via guarded recursion (REM), p. 10.
LICS-CSL-2014-Munch-Maccagnoni: Formulae-as-types for an involutive negation (GMM), p. 10.
ICALP-v2-2013-Padovani: Fair Subtyping for Open Session Types (LP), pp. 373–384.
SEFM-2013-DardhaGL #component: A Type System for Components (OD, EG, ML), pp. 167–181.
TLCA-2013-DudderMR: Intersection Type Matching with Subtyping (BD, MM, JR), pp. 125–139.
TLCA-2013-FridlenderP #algorithm #evaluation #normalisation: A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation (DF, MP), pp. 140–155.
DHM-HB-2013-KimATBHJ #performance #process: The Effects of Touch Screen Virtual Keyboard Key Sizes on Typing Performance, Typing Biomechanics and Muscle Activity (JHK, LSA, OT, MCB, CAH, PWJ), pp. 239–244.
PEPM-2013-Lopez-FraguasM #evaluation #functional: Typing as functional-logic evaluation (FJLF, EMM), pp. 23–32.
PEPM-2013-SagonasST #fault #precise: Precise explanation of success typing errors (KFS, JS, ST), pp. 33–42.
SAC-OOPS-J-2009-SaitoI13: Matching MyType to subtyping (CS, AI), pp. 933–952.
ASE-2013-Xiao0LLS #learning #named: TzuYu: Learning stateful typestates (HX, JS, YL, SWL, CS), pp. 432–442.
ESOP-2013-SchererR #data type: GADTs Meet Subtyping (GS, DR), pp. 554–573.
FoSSaCS-2013-HainryMP #analysis #complexity #process: Type-Based Complexity Analysis for Fork Processes (EH, JYM, RP), pp. 305–320.
CSL-2013-Leivant #induction #semantics: Global semantic typing for inductive and coinductive computing (DL), pp. 469–483.
CSL-2013-WangB #decidability #equation #semantics: Semantics of Intensional Type Theory extended with Decidable Equational Theories (QW, BB), pp. 653–667.
LICS-2013-BirkedalM #fixpoint #recursion: Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes (LB, REM), pp. 213–222.
LICS-2013-Kobayashi: Pumping by Typing (NK0), pp. 398–407.
LICS-2013-LicataS: Calculating the Fundamental Group of the Circle in Homotopy Type Theory (DRL, MS), pp. 223–232.
LICS-2013-Sacchini #calculus: Type-Based Productivity of Stream Definitions in the Calculus of Constructions (JLS), pp. 233–242.
VMCAI-2013-Pearce: Sound and Complete Flow Typing with Unions, Intersections and Negations (DJP), pp. 335–354.
VLDB-2012-Bidoit-TolluCU #detection #independence #xml: Type-Based Detection of XML Query-Update Independence (NBT, DC, FU), pp. 872–883.
ICPC-2012-KleinschmagerHRS #empirical #maintenance #static typing: Do static type systems improve the maintainability of software systems? An empirical study (SK, SH, RR, ÉT, AS), pp. 153–162.
ICFP-2012-ChenEW #λ-calculus: An error-tolerant type system for variational λ calculus (SC, ME, EW), pp. 29–40.
ICFP-2012-HenryMCM: Typing unmarshalling without marshalling types (GH, MM, EC, PM), pp. 287–298.
ICFP-2012-SeveriV #finite #normalisation #recursion: Pure type systems with corecursion on streams: from finite to infinitary normalisation (PS, FJdV), pp. 141–152.
CHI-2012-FindlaterW #adaptation #automation #personalisation: Personalized input: improving ten-finger touchscreen typing through automatic adaptation (LF, JOW), pp. 815–824.
CHI-2012-HenzeRB #behaviour #mobile #using: Observational and experimental investigation of typing behaviour using virtual keyboards for mobile devices (NH, ER, SB), pp. 2659–2668.
CHI-2012-KumarPL #interactive #speech: Voice typing: a new speech interaction model for dictation on touchscreen devices (AK, TP, BL), pp. 2277–2286.
CHI-2012-NicolauJ #comprehension #using: Touch typing using thumbs: understanding the effect of mobility and hand posture (HN, JAJ), pp. 2683–2686.
CHI-2012-RaihaO #case study #fault: An exploratory study of eye typing fundamentals: dwell time, text entry rate, errors, and workload (KJR, SO), pp. 3001–3010.
CSCW-2012-McDonaldGZ #analysis #prototype #social: Building for social translucence: a domain analysis and prototype system (DWM, SG, MZ), pp. 637–646.
ECMFA-2012-GuyCDSJ #on the: On Model Subtyping (CG, BC, SD, JS, JMJ), pp. 400–415.
ICMT-2012-VallecilloG #model transformation #using: Typing Model Transformations Using Tracts (AV, MG), pp. 56–71.
OOPSLA-2012-MayerHRTS #empirical #static typing #usability: An empirical study of the influence of static type systems on the usability of undocumented software (CM, SH, RR, ÉT, AS), pp. 683–702.
OOPSLA-2012-SuenagaFI #concurrent: Type-based safe resource deallocation for shared-memory concurrency (KS, RF, AI), pp. 1–20.
OOPSLA-2012-TakikawaSDTF: Gradual typing for first-class classes (AT, TSS, CD, STH, MF), pp. 793–810.
TOOLS-EUROPE-2012-MehnertA #using #verification: Verification of Snapshotable Trees Using Access Permissions and Typestate (HM, JA), pp. 187–201.
PADL-2012-St-AmourTFF: Typing the Numeric Tower (VSA, STH, MF, MF), pp. 289–303.
PEPM-2012-CaretteS #towards: Towards typing for small-step direct reflection (JC, AS), pp. 93–96.
POPL-2012-BhatAVG #probability: A type theory for probability density functions (SB, AA, RWV, AGG), pp. 545–556.
POPL-2012-ChughRJ #logic: Nested refinements: a logic for duck typing (RC, PMR, RJ), pp. 231–244.
POPL-2012-LicataH #2d: Canonicity for 2-dimensional type theory (DRL, RH), pp. 337–348.
POPL-2012-NadenBAB: A type system for borrowing permissions (KN, RB, JA, KB), pp. 557–570.
SAC-2012-DamianiPW #object-oriented #programming: A type system for checking specialization of packages in object-oriented programming (FD, APH, YW), pp. 1737–1742.
SLE-2012-BettiniSVC #implementation #tool support #xtext: Approaches and Tools for Implementing Type Systems in Xtext (LB, DS, MV, SC), pp. 392–412.
ICLP-2012-Hadjichristodoulou #polymorphism #prolog: A Gradual Polymorphic Type System with Subtyping for Prolog (SH), pp. 451–457.
ISSTA-2012-PradelHG #detection #parametricity #static analysis: Static detection of brittle parameter typing (MP, SH, TRG), pp. 265–275.
LICS-2012-AwodeyGS #induction: Inductive Types in Homotopy Type Theory (SA, NG, KS), pp. 95–104.
LICS-2012-JaberTS: Extending Type Theory with Forcing (GJ, NT, MS), pp. 395–404.
IFM-J-2009-DovlandJOS11 #behaviour #incremental #inheritance #lazy evaluation #multi #reasoning: Incremental reasoning with lazy behavioral subtyping for multiple inheritance (JD, EBJ, OO, MS), pp. 915–941.
TLCA-2011-ArndtK #formal method #modelling: Homotopy-Theoretic Models of Type Theory (PA, KK), pp. 45–60.
ICFP-2011-CastagnaX #morphism #parametricity #polymorphism: Set-theoretic foundation of parametric polymorphism and subtyping (GC, ZX), pp. 94–106.
ICFP-2011-GesbertGL #logic #morphism #parametricity #polymorphism #semantics: Parametric polymorphism and semantic subtyping: the logical connection (NG, PG, NL), pp. 107–116.
ICFP-2011-MaterzokB #continuation: Subtyping delimited continuations (MM, DB), pp. 81–93.
CHI-2011-FindlaterWW: Typing on flat glass: examining ten-finger expert typing patterns on touch surfaces (LF, JOW, DW), pp. 2453–2462.
DHM-2011-QinTD #using: The Upper Extremity Loading during Typing Using One, Two and Three Fingers (JQ, MT, JTD), pp. 178–185.
ICEIS-J-2011-Li11f #analysis #approach #case study #machine learning #using: A Study on Noisy Typing Stream Analysis Using Machine Learning Approach (JL0), pp. 149–161.
ECOOP-2011-WolffGTA: Gradual Typestate (RW, RG, ÉT, JA), pp. 459–483.
OOPSLA-2011-ImNGP #recursion: A syntactic type system for recursive modules (HI, KN, JG, SP), pp. 993–1012.
OOPSLA-2011-InaI: Gradual typing for generics (LI, AI), pp. 609–624.
OOPSLA-2011-SummersM #lightweight: Freedom before commitment: a lightweight type system for object initialisation (AJS, PM), pp. 1013–1032.
PLDI-2011-BeckmanN #composition #probability #scalability #specification: Probabilistic, modular and scalable inference of typestate specifications (NEB, AVN), pp. 211–221.
PLDI-2011-TateLL #java: Taming wildcards in Java’s type system (RT, AL, SL), pp. 614–627.
POPL-2011-RamseyD #composition #dependent type #independence #low level #using: Resourceable, retargetable, modular instruction selection using a machine-independent, type-based tiling of low-level intermediate code (NR, JD), pp. 575–586.
PPDP-2011-BiernackaBL #continuation: Typing control operators in the CPS hierarchy (MB, DB, SL), pp. 149–160.
PPDP-2011-ToninhoCP #linear: Dependent session types via intuitionistic linear type theory (BT, LC, FP), pp. 161–172.
SAC-2011-HauptPH #approach #programming language: Type harvesting: a practical approach to obtaining typing information in dynamic programming languages (MH, MP, RH), pp. 1282–1289.
GPCE-J-2005-LutterothDW11 #generative: A type system for reflective program generators (CL, DD, GW), pp. 392–422.
LDTA-2011-MametjanovWL #precise: More precise typing of rewrite strategies (AM, VLW, RL), p. 3.
ASPLOS-2011-GaoZCZQ #concurrent #debugging #named #towards: 2ndStrike: toward manifesting hidden concurrency typestate bugs (QG, WZ, ZC, MZ, FQ), pp. 239–250.
CASE-2011-MaramisDLK #automation: A system for automatic HPV typing via PCR-RFLP gel electrophoresis (CM, AD, AFL, SPK), pp. 549–556.
ESOP-2011-BonoMP #message passing: Typing Copyless Message Passing (VB, CM, LP), pp. 57–76.
ESOP-2011-CairesPSVF #data access: Type-Based Access Control in Data-Centric Systems (LC, JAP, JCS, HTV, LF), pp. 136–155.
ESOP-2011-GuhaSK #analysis #using: Typing Local Control and State Using Flow Analysis (AG, CS, SK), pp. 256–275.
ESOP-2011-HuntS #exponential #polynomial #security: From Exponential to Polynomial-Time Security Typing via Principal Types (SH, DS), pp. 297–316.
FoSSaCS-2011-Abel #similarity: Irrelevance in Type Theory with a Heterogeneous Equality Judgement (AA0), pp. 57–71.
FoSSaCS-2011-BernardyL #parametricity: Realizability and Parametricity in Pure Type Systems (JPB, ML), pp. 108–122.
LICS-2011-BarrasJSW #decidability #first-order #higher-order #named: CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory (BB, JPJ, PYS, QW), pp. 143–151.
LICS-2011-Marion #analysis #complexity: A Type System for Complexity Flow Analysis (JYM), pp. 123–132.
SIGMOD-2010-ZhouCC #named #prototype #query: DoCQS: a prototype system for supporting data-oriented content query (MZ, TC, KCCC), pp. 1211–1214.
ICFP-2010-BiermanGHL #semantics #smt: Semantic subtyping with an SMT solver (GMB, ADG, CH, DEL), pp. 105–116.
ILC-2010-Mehnert #detection #fault #type inference: Extending Dylan’s type system for better type inference and error detection (HM), pp. 1–10.
ECOOP-2010-Hanenberg #developer #empirical #programming #static typing: Doubts about the Positive Impact of Static Type Systems on Programming Tasks in Single Developer Projects — An Empirical Study (SH), pp. 300–303.
ECOOP-2010-VaziriTDHV: A Type System for Data-Centric Synchronization (MV, FT, JD, CH, JV), pp. 304–328.
OOPSLA-2010-Hanenberg #development #empirical #static typing: An experiment about static and dynamic type systems: doubts about the positive impact of static type systems on development time (SH), pp. 22–35.
OOPSLA-2010-MatsakisG: A time-aware type system for data-race protection and guaranteed initialization (NDM, TRG), pp. 634–651.
AdaEurope-2010-HongHBB #ada #named #programming: AdaStreams: A Type-Based Programming Extension for Stream-Parallelism with Ada 2005 (GH, KH, BB, JB), pp. 208–221.
POPL-2010-BhargavanFG #composition #protocol #security #verification: Modular verification of security protocol code by typing (KB, CF, ADG), pp. 445–456.
POPL-2010-Hutchins: Pure subtype systems (DSH), pp. 287–298.
SAC-OOPS-J-2008-HallettLRS10 #multi: Integrating coercion with subtyping and multiple dispatch (JJH, VL, SR, GLSJ), pp. 787–795.
FSE-2010-ErnstA #using: Building and using pluggable type systems (MDE, MA), pp. 375–376.
ICSE-2010-Bodden #analysis #hybrid #performance: Efficient hybrid typestate analysis by determining continuation-equivalent states (EB), pp. 5–14.
LDTA-2010-HoldermansH #on the #program transformation: On the rôle of minimal typing derivations in type-driven program transformation (SH, JH), p. 2.
IJCAR-2010-ShermanGD #partial order: A Slice-Based Decision Procedure for Type-Based Partial Orders (ES, BJG, MBD), pp. 156–170.
LICS-2010-SilesH #similarity: Equality Is Typable in Semi-full Pure Type Systems (VS, HH), pp. 21–30.
TLCA-2009-AbelCP #algorithm #composition #proving: A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (AA, TC, MP), pp. 5–19.
TLCA-2009-AwodeyR #semantics: Kripke Semantics for Martin-Löf’s Extensional Type Theory (SA, FR), pp. 249–263.
TLCA-2009-FujitaS: Existential Type Systems with No Types in Terms (KeF, AS), pp. 112–126.
TLCA-2009-Lumsdaine: Weak ω-Categories from Intensional Type Theory (PLL), pp. 172–187.
TLCA-2009-Petit #polymorphism #λ-calculus: A Polymorphic Type System for the λ-Calculus with Constructors (BP), pp. 234–248.
CHI-2009-MajarantaAS #performance: Fast gaze typing with an adjustable dwell time (PM, UKA, OS), pp. 357–360.
CIKM-2009-PinchakRL #information retrieval: Answer typing for information retrieval (CP, DR, DL), pp. 1955–1958.
ICMT-2009-VignagaJBB #model management: Typing in Model Management (AV, FJ, MCB, HB), pp. 197–212.
ECOOP-2009-AnconaL #induction #object-oriented: Coinductive Type Systems for Object-Oriented Languages (DA, GL), pp. 2–26.
ECOOP-2009-HaackP #flexibility: Type-Based Object Immutability with Flexible Initialization (CH, EP), pp. 520–545.
OOPSLA-2009-DucournauMP #assessment #empirical #implementation #inheritance #multi #object-oriented #static typing: Empirical assessment of object-oriented implementations with multiple inheritance and static typing (RD, FM, JP), pp. 41–60.
OOPSLA-2009-FurrAF #scripting language #static typing: Profile-guided static typing for dynamic scripting languages (MF, Jh(A, JSF), pp. 283–300.
PEPM-2009-MatsudaHT #xml: Type-based specialization of xml transformations (KM, ZH, MT), pp. 61–72.
PLDI-2009-KawaguchiRJ #data type #verification: Type-based data structure verification (MK, PMR, RJ), pp. 304–315.
ASE-2009-AnCF #ruby #static typing: Static Typing for Ruby on Rails (Jh(A, AC, JSF), pp. 590–594.
SAC-2009-AraujoSSF #classification #named #sequence: HIVSetSubtype: software for subtype classification of HIV-1 sequences (LVdA, SSS, ECS, JEF), pp. 811–815.
SAC-2009-SaitoI: Matching ThisType to subtyping (CS, AI), pp. 1851–1858.
ESOP-2009-KikuchiK #authentication #automation #encryption #protocol #verification: Type-Based Automated Verification of Authenticity in Cryptographic Protocols (DK, NK), pp. 222–236.
ESOP-2009-MalayeriA #empirical: Is Structural Subtyping Useful? An Empirical Study (DM, JA), pp. 95–111.
ESOP-2009-MostrousYH #commutative: Global Principal Typing in Partially Commutative Asynchronous Sessions (DM, NY, KH), pp. 316–332.
CSL-2009-Coquand: Forcing and Type Theory (TC), p. 2.
LICS-2009-KobayashiO #calculus #higher-order #model checking #recursion #μ-calculus: A Type System Equivalent to the Modal μ-Calculus Model Checking of Higher-Order Recursion Schemes (NK, CHLO), pp. 179–188.
FM-2008-DovlandJOS #behaviour #lazy evaluation: Lazy Behavioral Subtyping (JD, EBJ, OO, MS), pp. 52–67.
FLOPS-2008-AbelCD #algebra #on the #proving: On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory (AA, TC, PD), pp. 3–13.
FLOPS-2008-Benton #dynamic typing: Undoing Dynamic Typing (NB), pp. 224–238.
FLOPS-2008-Kobayashi #program analysis: Substructural Type Systems for Program Analysis (NK), p. 14.
Haskell-2008-AhnS #algebra #data type #recursion: Shared subtypes: subtyping recursive parametrized algebraic data types (KYA, TS), pp. 75–86.
CHI-2008-ClawsonLRIS #automation #fault #using: Automatic whiteout++: correcting mini-QWERTY typing errors using keypress timing (JC, KL, AR, RAI, TS), pp. 573–582.
CHI-2008-MorrisBM #named #using: SuperBreak: using interactivity to enhance ergonomic typing breaks (DM, AJBB, BM), pp. 1817–1826.
ECOOP-2008-MalayeriA: Integrating Nominal and Structural Subtyping (DM, JA), pp. 260–284.
OOPSLA-2008-BeckmanBA #verification: Verifying correct usage of atomic blocks and typestate (NEB, KB, JA), pp. 227–244.
OOPSLA-2008-GilM #java #named: Whiteoak: introducing structural typing into java (JYG, IM), pp. 73–90.
OOPSLA-2008-RobersonHDB #model checking #performance: Efficient software model checking of soundness of type systems (MR, MH, PTD, CB), pp. 493–504.
PPDP-2008-MontenegroPS #correctness #memory management #proving: A type system for safe memory management and its proof of correctness (MM, RP, CS), pp. 152–162.
SAS-2008-CominiDV #abstract interpretation #on the #polymorphism #recursion: On Polymorphic Recursion, Type Systems, and Abstract Interpretation (MC, FD, SV), pp. 144–158.
SAS-2008-RuggieriM #constraints #linear #source code: Typing Linear Constraints for Moding CLP() Programs (SR, FM), pp. 128–143.
ASE-2008-JoshiS #java #parallel #predict #source code #thread: Predictive Typestate Checking of Multithreaded Java Programs (PJ, KS), pp. 288–296.
SAC-2008-BaveraB #analysis #bytecode #data flow #policy: Type-based information flow analysis for bytecode languages with variable object field policies (FB, EB), pp. 347–351.
SAC-2008-HallettLRS #multi: Integrating coercion with subtyping and multiple dispatch (JJH, VL, SR, GLSJ), pp. 166–170.
GPCE-2008-LienhardtSS #communication #component: Typing communicating component assemblages (ML, AS, JBS), pp. 125–136.
LCTES-2008-DelavalGP #automation #data flow #higher-order #source code: A type system for the automatic distribution of higher-order synchronous dataflow programs (GD, AG, MP), pp. 101–110.
ESOP-2008-Boudol: Typing Safe Deallocation (GB), pp. 116–130.
ESOP-2008-Cheney #query #regular expression #xml: Regular Expression Subtyping for XML Query and Update Languages (JC), pp. 32–47.
ESOP-2008-PetersenBNM #hoare: A Realizability Model for Impredicative Hoare Type Theory (RLP, LB, AN, GM), pp. 337–352.
FoSSaCS-2008-Mishra-LingerS #morphism #polymorphism: Erasure and Polymorphism in Pure Type Systems (NML, TS), pp. 350–364.
CAV-2008-KobayashiS #hybrid #mobile #process: A Hybrid Type System for Lock-Freedom of Mobile Processes (NK, DS), pp. 80–93.
CSL-2008-AbelR #higher-order: Syntactic Metatheory of Higher-Order Subtyping (AA, DR), pp. 446–460.
CSL-2008-BartheGR #termination: Type-Based Termination with Sized Products (GB, BG, CR), pp. 493–507.
LICS-2008-Burel #deduction #first-order #representation #using: A First-Order Representation of Pure Type Systems Using Superdeduction (GB), pp. 253–263.
ICALP-2007-KobayashiS #behaviour #calculus: Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the π -Calculus (NK, TS), pp. 740–751.
TLCA-2007-Baillot #linear #logic #polynomial: From Proof-Nets to Linear Logic Type Systems for Polynomial Time Computing (PB), pp. 2–7.
TLCA-2007-CousineauD #calculus: Embedding Pure Type Systems in the λ-π-Calculus Modulo (DC, GD), pp. 102–117.
TLCA-2007-KiselyovS #continuation: A Substructural Type System for Delimited Continuations (OK, CcS), pp. 223–239.
TLCA-2007-MostrousY #higher-order #mobile #process: Two Session Typing Systems for Higher-Order Mobile Processes (DM, NY), pp. 321–335.
ICFP-2007-Dreyer #recursion: A type system for recursive modules (DD), pp. 289–302.
ICFP-2007-Pfenning #revisited: Subtyping and intersection types revisited (FP), p. 219.
IFL-2007-VriesPA: Uniqueness Typing Simplified (EdV, RP, DMA), pp. 201–218.
HIMI-IIE-2007-MyojinNKN #human-computer #interactive #process #prototype: Friendly Process of Human-Computer Interaction — A Prototype System in Nostalgic World (SM, MN, HK, SN), pp. 102–109.
MoDELS-2007-SteimannK #modelling: Piecewise Modelling with State Subtypes (FS, TK), pp. 181–195.
MoDELS-2007-SteimannK #modelling: Piecewise Modelling with State Subtypes (FS, TK), pp. 181–195.
ECOOP-2007-SiekT: Gradual Typing for Objects (JGS, WT), pp. 2–27.
OOPSLA-2007-BierhoffA #alias #composition: Modular typestate checking of aliased objects (KB, JA), pp. 301–320.
LOPSTR-2007-AlbertGGP #online #partial evaluation: Type-Based Homeomorphic Embedding and Its Applications to Online Partial Evaluation (EA, JPG, MGZ, GP), pp. 23–42.
POPL-2007-AppelMRV: A very modal model of a modern, major, general type system (AWA, PAM, CDR, JV), pp. 109–122.
PPDP-2007-Hamana #data type #higher-order #induction #semantics: Higher-order semantic labelling for inductive datatype systems (MH), pp. 97–108.
ASE-2007-DwyerP #cost analysis #dynamic analysis #static analysis: Residual dynamic typestate analysis exploiting static analysis: results to reformulate and reduce the cost of dynamic analysis (MBD, RP), pp. 124–133.
SAC-2007-Lu #implementation: Implementing type-based constructive negation (LL), pp. 1299–1306.
LCTES-2007-PermandlaRB #java #virtual machine: A type system for preventing data races and deadlocks in the java virtual machine language: 1 (PP, MR, CB), p. 10.
ESOP-2007-NanevskiAMB #data type #hoare: Abstract Predicates and Mutable ADTs in Hoare Type Theory (AN, AA, GM, LB), pp. 189–204.
ESOP-2007-SuenagaK #analysis #calculus #concurrent: Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts (KS, NK), pp. 490–504.
LICS-2007-AbelCD #evaluation #normalisation #similarity: Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements (AA, TC, PD), pp. 3–12.
TAP-2007-Haiyan #algorithm #distributed #proving #testing: Testing and Proving Distributed Algorithms in Constructive Type Theory (QH), pp. 79–94.
VLDB-2006-BenzakenCCN #xml: Type-Based XML Projection (VB, GC, DC, KN), pp. 271–282.
RTA-2006-Salvati #equation #linear #λ-calculus: Syntactic Descriptions: A Type System for Solving Matching Equations in the Linear λ-Calculus (SS), pp. 151–165.
FLOPS-2006-GregoireTW #approach: A Computational Approach to Pocklington Certificates in Type Theory (BG, LT, BW), pp. 97–113.
ICFP-2006-DenielouL #abstraction #distributed: Abstraction preservation and subtyping in distributed languages (PMD, JJL), pp. 286–297.
ICFP-2006-NanevskiMB #hoare #morphism #polymorphism: Polymorphism and separation in hoare type theory (AN, GM, LB), pp. 62–73.
ICFP-2006-WalkerMLRA #static typing #λ-calculus: Static typing for a faulty λ calculus (DW, LWM, JL, GAR, DIA), pp. 38–49.
IFL-2006-Kozsik #proving: Proving Program Properties Specified with Subtype Marks (TK), pp. 163–180.
IFL-2006-VriesPA: Uniqueness Typing Redefined (EdV, RP, DMA), pp. 181–198.
ICEIS-HCI-2006-FrangeskidesL #interactive #multi #prototype: Multi-Modal Hands-Free Human Computer Interaction: A Prototype System (FF, AL), pp. 19–26.
OOPSLA-2006-AndreaeNMM #framework #implementation: A framework for implementing pluggable type systems (CA, JN, SM, TDM), pp. 57–74.
POPL-2006-KimYC #multi #polymorphism: A polymorphic modal type system for lisp-like multi-staged languages (ISK, KY, CC), pp. 257–268.
PPDP-2006-Hanus #user interface #web: Type-oriented construction of web user interfaces (MH), pp. 27–38.
PPDP-2006-MatsunoO: A type system equivalent to static single assignment (YM, AO), pp. 249–260.
PPDP-2006-YuseI #generative #multi #persistent: A modal type system for multi-level generating extensions with persistent code (YY, AI), pp. 201–212.
ICSE-2006-JiangS #c #correctness #named #source code #validation: Osprey: a practical type system for validating dimensional unit correctness of C programs (LJ, ZS), pp. 262–271.
CC-2006-Necula #dependent type #low level #using: Using Dependent Types to Port Type Systems to Low-Level Languages (GCN), p. 1.
ESOP-2006-HofmannJ #analysis: Type-Based Amortised Heap-Space Analysis (MH, SJ), pp. 22–37.
CSL-2006-LengrandDM #calculus: A Sequent Calculus for Type Theory (SL, RD, JM), pp. 441–455.
IJCAR-2006-Brown #set: Combining Type Theory and Untyped Set Theory (CEB), pp. 205–219.
ISSTA-2006-FinkYDRG #alias #effectiveness #verification: Effective typestate verification in the presence of aliasing (SJF, EY, ND, GR, EG), pp. 133–144.
VLDB-2005-CataniaMM #named #prototype: PSYCHO: A Prototype System for Pattern Management (BC, AM, MM), pp. 1346–1349.
ICALP-2005-CastagnaF #semantics: A Gentle Introduction to Semantic Subtyping (GC, AF), pp. 30–34.
TLCA-2005-BaillotT #algorithm #logic: A Feasible Algorithm for Typing in Elementary Affine Logic (PB, KT), pp. 55–70.
TLCA-2005-BartheGP #polymorphism #termination: Practical Inference for Type-Based Termination in a Polymorphic Setting (GB, BG, FP), pp. 71–85.
TLCA-2005-CosmoPR #commutative #recursion: Subtyping Recursive Types Modulo Associative Commutative Products (RDC, FP, DR), pp. 179–193.
CEFP-2005-Kozsik #tutorial: Tutorial on Subtype Marks (TK), pp. 191–222.
Haskell-2005-AbelBBHN #haskell #source code #using #verification: Verifying haskell programs using constructive type theory (AA0, MB, AB, JH, UN), pp. 62–73.
MoDELS-2005-SteelJ #modelling #reuse: Model Typing for Improving Reuse in Model-Driven Engineering (JS, JMJ), pp. 84–96.
MoDELS-2005-SteelJ #modelling #reuse: Model Typing for Improving Reuse in Model-Driven Engineering (JS, JMJ), pp. 84–96.
ECOOP-2005-LuP #reachability: A Type System for Reachability and Acyclicity (YL, JP), pp. 479–503.
OOPSLA-2005-NandaGC: Deriving object typestates in the presence of inter-object references (MGN, CG, SC), pp. 77–96.
LOPSTR-2005-GallagherPA #abstract domain: Converting One Type-Based Abstract Domain to Another (JPG, GP, EA), pp. 147–162.
LOPSTR-2005-SuenagaKY #approach #automation #generative #source code: Extension of Type-Based Approach to Generation of Stream-Processing Programs by Automatic Insertion of Buffering Primitives (KS, NK, AY), pp. 98–114.
POPL-2005-Goguen #approach #similarity: A syntactic approach to eta equality in type theory (HG), pp. 75–84.
PPDP-2005-CastagnaF #semantics: A gentle introduction to semantic subtyping (GC, AF), pp. 198–199.
PPDP-2005-Wojciechowski #transaction #version control: Isolation-only transactions by typing and versioning (PTW), pp. 70–81.
ESEC-FSE-2005-BierhoffA #lightweight #specification: Lightweight object specification with typestates (KB, JA), pp. 217–226.
SAC-OOPS-J-2005-BettiniBL #flexibility: Safe and Flexible Objects with Subtyping (LB, VB, SL), pp. 5–29.
SAC-OOPS-J-2005-KaminaT #flexibility #mixin: Flexible Method Combination based on Mixin Subtyping (TK, TT), pp. 95–115.
GPCE-2005-BravenboerVVV #ambiguity #metaprogramming #source code #syntax: Generalized Type-Based Disambiguation of Meta Programs with Concrete Object Syntax (MB, RV, JJV, EV), pp. 157–172.
GPCE-2005-DraheimLW #generative: A Type System for Reflective Program Generators (DD, CL, GW), pp. 327–341.
PPoPP-2005-SasturkarAWS #analysis #automation: Automated type-based analysis of data races and atomicity (AS, RA, LW, SDS), pp. 83–94.
ESOP-2005-MakholmW #calculus #mobile #polymorphism #process #reduction: Instant Polymorphic Type Systems for Mobile Process Calculi: Just Add Reduction Rules and Close (HM, JBW), pp. 389–407.
ESOP-2005-NaikP #model checking: A Type System Equivalent to a Model Checker (MN, JP), pp. 374–388.
ESOP-2005-NiehrenPS #complexity #satisfiability: Complexity of Subtype Satisfiability over Posets (JN, TP, ZS), pp. 357–373.
ESOP-2005-SecoC #component #polymorphism: Subtyping First-Class Polymorphic Components (JCS, LC), pp. 342–356.
ESOP-2005-Thiemann #javascript #source code #towards: Towards a Type System for Analyzing JavaScript Programs (PT), pp. 408–422.
CADE-2005-Brown #reasoning #similarity: Reasoning in Extensional Type Theory with Equality (CEB), pp. 23–37.
ICLP-2005-CoqueryF: A Type System for CHR (EC, FF), pp. 402–403.
LICS-2005-BirkedalTY #higher-order #semantics: Semantics of Separation-Logic Typing and Higher-Order Frame Rules (LB, NTS, HY), pp. 260–269.
LICS-2005-CastagnaNV #calculus #semantics: Semantic Subtyping for the p-Calculus (GC, RDN, DV), pp. 92–101.
VMCAI-2005-LamKR #consistency #data type: Generalized Typestate Checking for Data Structure Consistency (PL, VK, MCR), pp. 430–447.
ICALP-2004-Hofmann #logic #question #what: What Do Program Logics and Type Systems Have in Common? (MH0), pp. 4–7.
RTA-2004-Blanqui #higher-order #term rewriting #termination: A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems (FB), pp. 24–39.
AFP-2004-DijkstraS04 #attribute grammar #haskell: Typing Haskell with an Attribute Grammar (AD, SDS), pp. 1–72.
ICFP-2004-NeergaardM #why: Types, potency, and idempotency: why nonlinearity and amnesia make a type system work (PMN, HGM), pp. 138–149.
ICGT-2004-Klempien-HinrichsKK #graph transformation: Typing of Graph Transformation Units (RKH, HJK, SK), pp. 112–127.
CHI-2004-LyonsSPFLDL #mobile: Twiddler typing: one-handed chording text entry for mobile phones (KL, TS, DP, JF, AL, AD, EWL), pp. 671–678.
EDOC-2004-HoffnerFF #flexibility: Strong and Flexible Domain Typing for Dynamic E-Business (YH, SF, CF), pp. 98–107.
ECOOP-2004-DeLineF: Typestates for Objects (RD, MF), pp. 465–490.
ECOOP-2004-FindlerFF #contract #semantics: Semantic Casts: Contracts and Structural Subtyping in a Nominal World (RBF, MF, MF), pp. 364–388.
OOPSLA-2004-BirkaE: A practical type system and language for reference immutability (AB, MDE), pp. 35–49.
PADL-2004-ElsmanL #html #ml #web: Typing XHTML Web Applications in ML (ME, KFL), pp. 224–238.
PEPM-2004-PopeeaC #correctness #protocol #proving #verification: A type system for resource protocol verification and its correctness proof (CP, WNC), pp. 135–146.
POPL-2004-Dreyer #recursion: A type system for well-founded recursion (DD), pp. 293–305.
FSE-2004-EdwardsJT #modelling: A type system for object models (JE, DJ, ET), pp. 189–199.
SAC-2004-JezierskiMW #database #maintenance #object-oriented #prototype: Prototype system for method materialisation and maintenance in object-oriented databases (JJ, MM, RW), pp. 1323–1327.
ESOP-2004-CarlierPWK #flexibility #linear: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types (SC, JP, JBW, AJK), pp. 294–309.
FASE-2004-GhezziMP #static analysis: Enhancing Remote Method Invocation through Type-Based Static Analysis (CG, VM, GPP), pp. 339–353.
CSL-2004-SchoppS #dependent type: A Dependent Type Theory with Names and Binding (US, IS), pp. 235–249.
CSL-2004-Vouillon: Subtyping Union Types (JV), pp. 415–429.
PODS-2003-Segoufin #bound #complexity #documentation #query #xml: Typing and querying XML documents: some complexity bounds (LS), pp. 167–178.
SCAM-2003-OlmosV #compilation #dynamic typing #static typing: Turning Dynamic Typing into Static Typing by Program Specialization in a Compiler Front-end for Octave (KO, EV), pp. 141–150.
ICALP-2003-GutierrezR #calculus: Expansion Postponement via Cut Elimination in Sequent Calculi for Pure Type Systems (FG, BCR), pp. 956–968.
TLCA-2003-CoppolaR #logic: Principal Typing in Elementary Affine Logic (PC, SRDR), pp. 90–104.
ICFP-2003-HiguchiO #data access #static typing #virtual machine: A static type system for JVM access control (TH, AO), pp. 227–237.
ECOOP-2003-LamR #analysis #automation #design: A Type System and Analysis for the Automatic Extraction and Enforcement of Design Information (PL, MCR), pp. 275–302.
ECOOP-2003-PalaczV #java #realtime #testing: Java Subtype Tests in Real-Time (KP, JV), pp. 378–404.
AdaEurope-2003-LinM #behaviour #object-oriented #programming: A Behavioural Notion of Subtyping for Object-Oriented Programming in SPARK95 (TML, JAM), pp. 309–321.
PADL-2003-CoelhoF #logic programming #xml: Type-Based XML Processing in Logic Programming (JC, MF), pp. 273–285.
POPL-2003-BartheCKL: Pure patterns type systems (GB, HC, CK, LL), pp. 250–261.
POPL-2003-Chen #calculus: Coercive subtyping for the calculus of constructions (GC), pp. 150–159.
POPL-2003-DreyerCH #higher-order: A type system for higher-order modules (DD, KC, RH), pp. 236–249.
POPL-2003-PetersenHCP #layout #memory management: A type theory for memory allocation and data layout (LP, RH, KC, FP), pp. 172–184.
SAS-2003-FieldGRY #abstraction #complexity #verification: Typestate Verification: Abstraction Techniques and Complexity Results (JF, DG, GR, EY), pp. 439–462.
SAS-2003-LiblitAY #distributed: Type Systems for Distributed Data Sharing (BL, AA, KAY), pp. 273–294.
ASE-2003-AhmadAGK #detection #fault #spreadsheet: A Type System for Statically Detecting Spreadsheet Errors (YA, TA, SG, SK), pp. 174–183.
GPCE-2003-ZolyomiPK #c++ #metaprogramming: An Extension to the Subtype Relationship in C++ Implemented with Template Metaprogramming (IZ, ZP, TK), pp. 209–227.
LICS-2003-Kopylov: Dependent Intersection: A New Way of Defining Records in Type Theory (AK), pp. 86–95.
LICS-2003-KuncakR #decidability #recursion: Structural Subtyping of Non-Recursive Types is Decidable (VK, MCR), pp. 96–107.
ICFP-2002-BaarsS #dynamic typing: Typing dynamic typing (AIB, SDS), pp. 157–166.
ICFP-2002-CraryV #scalability: An expressive, scalable type theory for certified code (KC, JV), pp. 191–205.
ICPR-v3-2002-ShiWOK02a #automation #prototype: Automatic Grading Prototype System for KANJI Dictation Test (MS, TW, WO, FK), pp. 232–235.
ECOOP-2002-IgarashiV #on the #parametricity: On Variance-Based Subtyping for Parametric Types (AI, MV), pp. 441–469.
ASIA-PEPM-2002-IwamaK #virtual machine: A new type system for JVM lock primitives (FI, NK), pp. 71–82.
LOPSTR-2002-GutierrezR #calculus #verification: A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen/Kleene (FG, BCR), pp. 17–31.
POPL-2002-ShaoSTP: A type system for certified binaries (ZS, BS, VT, NP), pp. 217–232.
POPL-2002-SuANPT #constraints #first-order: The first-order theory of subtyping constraints (ZS, AA, JN, TP, RT), pp. 203–216.
PPDP-2002-Chen #integration: Full integration of subtyping and if-expression (GC), pp. 181–188.
PPDP-2002-Shafarenko #morphism #type inference: Coercion as homomorphism: type inference in a system with subtyping and overloading (AVS), pp. 14–25.
ESOP-2002-AspinallH: Another Type System for In-Place Update (DA, MH), pp. 36–52.
ICLP-2002-CoqueryF #morphism #named #parametricity #polymorphism: TCLP: Overloading, Subtyping and Parametric Polymorphism Made Practical for CLP (EC, FF), p. 480.
LICS-2002-FrischCB #semantics: Semantic Subtyping (AF, GC, VB), pp. 137–146.
LICS-2002-PalsbergZ #performance #type inference: Efficient Type Inference for Record Concatenation and Subtyping (JP, TZ), pp. 125–136.
PASTE-2001-Palsberg #analysis: Type-based analysis and applications (JP), pp. 20–27.
WCRE-2001-Guilfanov #re-engineering: A Simple Type System for Program Reengineering (IG), pp. 357–361.
WCRE-2001-MycroftOK #decompiler: Comparing Type-Based and Proof-Directed Decompilation (AM, AO, SyK), pp. 362–367.
TLCA-2001-Chroboczek #game studies #recursion: Subtyping Recursive Games (JC), pp. 61–75.
TLCA-2001-CoppolaM #constraints #linear #logic: Typing λ Terms in Elementary Logic with Linear Constraints (PC, SM), pp. 76–90.
TLCA-2001-Geuvers #dependent type #higher-order #induction: Induction Is Not Derivable in Second Order Dependent Type Theory (HG), pp. 166–181.
TLCA-2001-Hofmann #behaviour #bound #complexity #memory management #using: From Bounded Arithmetic to Memory Management: Use of Type Theory to Capture Complexity Classes and Space Behaviour (MH0), pp. 2–3.
FLOPS-J1-1998-Tsukada01 #framework: Martin-Löf’s Type Theory as an Open-Ended Framework (YT), pp. 31–67.
ICFP-2001-Duggan: Type-Based Hot Swapping of Running Modules (DD), pp. 62–73.
IFL-2001-Minamide #behaviour #runtime: Runtime Behavior of Conversion Interpretation of Subtyping (YM), pp. 155–167.
IFL-2001-PenaS: Sized Types for Typing Eden Skeletons (RP, CS), pp. 1–17.
OOPSLA-2001-BoyapatiR #java #source code: A Parameterized Type System for Race-Free Java Programs (CB, MCR), pp. 56–69.
OOPSLA-2001-ZibinG #encoding #performance #testing: Efficient Subtyping Tests with PQ-Encoding (YZ, JYG), pp. 96–107.
LOPSTR-2001-Caldwell #recursion: Extracting General Recursive Program Schemes in Nuprl’s Type Theory (JLC), pp. 233–244.
POPL-2001-Gil: Subtyping arithmetical types (JYG), pp. 276–289.
POPL-2001-GordonS #multi: Typing a multi-language intermediate code (ADG, DS), pp. 248–260.
POPL-2001-IgarashiK #π-calculus: A generic type system for the π-calculus (AI, NK), pp. 128–141.
POPL-2001-RehofF #analysis #polymorphism: Type-base flow analysis: from polymorphic subtyping to CFL-reachability (JR, MF), pp. 54–66.
PPDP-2001-Gordon: Types for Cyphers: Thwarting Mischief and Malice with Type Theory (ADG), p. 136.
ESEC-FSE-2001-FindlerLF #behaviour #contract: Behavioral contracts and behavioral subtyping (RBF, ML, MF), pp. 229–236.
CC-2001-SchuppGML #generative: User-Extensible Simplification — Type-Based Optimizer Generators (SS, DG, DRM, SML), pp. 86–101.
ESOP-2001-XuRM: Typestate Checking of Machine Code (ZX, TWR, BPM), pp. 335–351.
FoSSaCS-2001-BartheP #dependent type #morphism #proving #reuse: Type Isomorphisms and Proof Reuse in Dependent Type Theory (GB, OP), pp. 57–71.
CSL-2001-KopylovN #markov: Markov’s Principle for Propositional Type Theory (AK, AN), pp. 570–584.
IJCAR-2001-AvronL #canonical: Canonical Propositional Gentzen-Type Systems (AA, IL), pp. 529–544.
LICS-2001-Jeffrey #induction #lts: A Symbolic Labelled Transition System for Coinductive Subtyping of Fμ≤ Types (AJ), pp. 323–333.
LICS-2001-Pfenning #proving: Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory (FP), pp. 221–230.
ICALP-2000-Konig #mobile #process: Analysing Input/Output-Capabilities of Mobile Processes with a Generic Type System (BK0), pp. 403–414.
ICFP-2000-Crary #compilation: Typed compilation of inclusive subtyping (KC), pp. 68–81.
ICFP-2000-GapeyevLP #functional #recursion: Recursive subtyping revealed: functional pearl (VG, MYL, BCP), pp. 221–231.
IFL-2000-GustavssonS #analysis #bound #morphism #polymorphism: A Usage Analysis with Bounded Usage Polymorphism and Subtyping (JG, JS), pp. 140–157.
ECOOP-2000-FisherR: Extending Moby with Inheritance-Based Subtyping (KF, JHR), pp. 83–107.
TOOLS-ASIA-2000-JiangLX #process #uml: Embedding UML and Type Theory to Formalize the Process of Requirement Engineering (HJ, DL, XX), pp. 32–39.
TOOLS-USA-2000-HeberleLNZ: Weak Subtyping and Genericity (AH, WL, RN, WZ), pp. 149–158.
TOOLS-USA-2000-SoundarajanF #behaviour #multi: Behavioral Subtyping and Behavioral Enrichment of Multimethods (NS, SF), p. 105–?.
PADL-2000-ChuangM #functional #programming: Out-of-Core Functional Programming with Type-Based Primitives (TRC, SCM), pp. 32–46.
PEPM-2000-Kobayashi: Type-Based Useless Variable Elimination (NK), pp. 84–93.
PLDI-2000-FlanaganF #concurrent #detection #java: Type-based race detection for Java (CF, SNF), pp. 219–232.
POPL-2000-KnoblockR #bytecode #java: Type Elaboration and Subtype Completion for Java Bytecode (TBK, JR), pp. 228–242.
POPL-2000-LiblitA #data type #distributed: Type Systems for Distributed Data Structures (BL, AA), pp. 199–213.
POPL-2000-SandholmS #documentation #web: A Type System for Dynamic Web Documents (AS, MIS), pp. 290–301.
POPL-2000-Walker #policy #security: A Type System for Expressive Security Policies (DW), pp. 254–267.
PPDP-2000-HanusS #functional #logic programming #nondeterminism #source code: Type-based nondeterminism checking in functional logic programs (MH, FS), pp. 202–213.
SAIG-2000-BerardiCDG #functional #source code: Type-Based Useless-Code Elimination for Functional Programs (SB, MC, FD, PG), pp. 172–189.
ESOP-2000-Hofmann #bound #functional: A Type System for Bounded Space and Functional In-Place Update--Extended Abstract (MH0), pp. 165–179.
FoSSaCS-2000-BartheR #calculus #induction: Constructor Subtyping in the Calculus of Inductive Constructions (GB, FvR), pp. 17–34.
FoSSaCS-2000-Damiani #rank: Typing Local Definitions and Conditional Expressions with Rank 2 Intersection (FD), pp. 82–97.
FoSSaCS-2000-MaiettiPR #category theory #linear #modelling: Categorical Models for Intuitionistic and Linear Type Theory (MEM, VdP, ER), pp. 223–237.
FoSSaCS-2000-Zimmer #algorithm #mobile: Subtyping and Typing Algorithms for Mobile Ambients (PZ), pp. 375–390.
TACAS-2000-XiongL #component #design: An Extensible Type System for Component-Based Design (YX, EAL), pp. 20–37.
CADE-2000-AndrewsBB #proving #theorem proving: System Description: TPS: A Theorem Proving System for Type Theory (PBA, MB, CEB), pp. 164–169.
CADE-2000-BezemHN #automation #proving #using: Automated Proof Construction in Type Theory Using Resolution (MB, DH, HdN), pp. 148–163.
CSL-2000-Aspinall: Subtyping with Power Types (DA), pp. 156–171.
CSL-2000-HancockS #dependent type #interactive #source code: Interactive Programs in Dependent Type Theory (PH, AS), pp. 317–331.
LICS-2000-Chroboczek #game studies #semantics: Game Semantics and Subtyping (JC), pp. 192–203.
LICS-2000-Miquel: A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping (AM), pp. 18–29.
TLCA-1999-Zwanenburg: Pure Type Systems with Subtyping (JZ), pp. 381–396.
ICFP-1999-KfouryMTW: Relating Typability and Expressiveness in Finite-Rank Intersection Type Systems (AJK, HGM, FAT, JBW), pp. 90–101.
ICFP-1999-WallaceR #combinator #haskell #question #xml: Haskell and XML: Generic Combinators or Type-Based Translation? (MW, CR), pp. 148–159.
CHI-1999-GoldsteinBAT #interface #mobile: Non-Keyboard QWERTY Touch Typing: A Portable Input Interface for The Mobile User (MG, RB, GA, ST), pp. 32–39.
OOPSLA-1999-Duggan #composition #java #reverse engineering: Modular Type-Based Reverse Engineering of Parameterized Types in Java Code (DD), pp. 97–113.
TOOLS-ASIA-1999-LiZL #communication #csp #process: The Typing of Communicating Sequential Processes (WL, XZ, SL), pp. 61–66.
PEPM-1999-Thiemann: Interpreting Specialization in Type Theory (PT), pp. 30–43.
POPL-1999-EidorffHMNST #named: AnnoDomini: From Type Theory to Year 2000 Conversion Tool (PHE, FH, CM, HN, MHS, MT), pp. 1–14.
POPL-1999-OCallahn #bytecode #java: A Simple, Comprehensive Type System for Java Bytecode Subroutines (RO), pp. 70–78.
POPL-1999-PessauxL #analysis #exception: Type-Based Analysis of Uncaught Exceptions (FP, XL), pp. 276–290.
POPL-1999-RielyH #mobile #trust: Trust and Partial Typing in Open Systems of Mobile Agents (JR, MH), pp. 93–104.
ESOP-1999-BartheF: Constructor Subtyping (GB, MJF), pp. 109–127.
ESOP-1999-GayH #interactive: Types and Subtypes for Client-Server Interactions (SJG, MH), pp. 74–90.
ESOP-1999-Mycroft #decompiler #re-engineering: Type-Based Decompilation (or Program Reconstruction via Type Reconstruction) (AM), pp. 208–223.
FoSSaCS-1999-Benke #algebra #ml: An Algebraic Characterization of Typability in ML with Subtyping (MB), pp. 104–119.
CSL-1999-CompagnoniG #higher-order #symmetry: Anti-Symmetry of Higher-Order Subtyping (ABC, HG), pp. 420–438.
CSL-1999-GeuversPZ #proving: Safe Proof Checking in Type Theory with Y (HG, EP, JZ), pp. 439–452.
CSL-1999-Howe #interactive #proving #theorem proving #using: Interactive Theorem Proving Using Type Theory (DJH), p. 578.
LICS-1999-Altenkirch #similarity: Extensional Equality in Intensional Type Theory (TA), pp. 412–420.
LICS-1999-ColazzoG #kernel #recursion: Subtyping Recursive Types in Kernel Fun (DC, GG), pp. 137–146.
HT-1998-FurtadoM #flexibility #hypermedia: Enforcing Strong Object Typing in Flexible Hypermedia (PF, HM), pp. 171–179.
ICALP-1998-Gimenez #recursion: Structural Recursive Definitions in Type Theory (EG), pp. 397–408.
ICALP-1998-HengleinR #automaton #complexity #constraints #recursion: Constraint Automata and the Complexity of Recursive Subtype Entailment (FH, JR), pp. 616–627.
ICALP-1998-Sewell #distributed #π-calculus: Global/Local Subtyping and Capability Inference for a Distributed π-calculus (PS), pp. 695–706.
FLOPS-1998-Takeuti: A Type Theory for Cyclic Strcture (IT), pp. 207–226.
ICFP-1998-Ennals98a: Verbose Typing (RE), p. 340.
ICFP-1998-Kieburtz #monad: Taming Effects with Monadic Typing (RBK), pp. 51–62.
ICFP-1998-Nordlander #polymorphism: Pragmatic Subtyping in Polymorphic Languages (JN), pp. 216–227.
ICFP-1998-Pottier #framework #type inference: A Framework for Type Inference with Subtyping (FP), pp. 228–238.
OOPSLA-1998-FreundM #bytecode #java: A Type System for Object Initialization in the Java Bytecode Language (SNF, JCM), pp. 310–327.
OOPSLA-1998-Litvinov #morphism #polymorphism #static typing #towards: Contraint-Based Polymorphism in Cecil: Towards a Practical and Static Type System (VL), pp. 388–411.
TOOLS-USA-1998-LoweNTZ #inheritance: Weak Subtyping — Yet Another Notion of Inheritance (WL, RN, MT, WZ), pp. 333–345.
PLDI-1998-DiwanMM #alias #analysis: Type-Based Alias Analysis (AD, KSM, JEBM), pp. 106–117.
POPL-1998-Nishimura #static typing: Static Typing for Dynamic Messages (SN), pp. 266–278.
POPL-1998-ShieldsSJ #dynamic typing #staged #type inference: Dynamic Typing as Staged Type Inference (MS, TS, SLPJ), pp. 289–302.
POPL-1998-StataA #bytecode #java: A Type System for Java Bytecode Subroutines (RS, MA), pp. 149–160.
SAS-1998-Duggan #finite #morphism #polymorphism #type inference: Finite Subtype Inference with Explicit Polymorphism (DD), pp. 295–310.
ESOP-1998-Remy: From Classes to Objects via Subtyping (DR), pp. 200–220.
FoSSaCS-1998-AmadioC #analysis: Analysis of a Guard Condition in Type Theory (RMA, SCG), pp. 48–62.
CSL-1998-Barthe #normalisation: Existence and Uniqueness of Normal Forms in Pure Type Systems with βη-Conversion (GB), pp. 241–259.
CSL-1998-Vorobyov #functional: Subtyping Functional+Nonempty Record Types (SGV), pp. 283–297.
JICSLP-1998-FagesP: A Generic Type System for CLP(chi) (FF, MP), pp. 353–354.
LICS-1998-BirkedalCRS #category theory: Type Theory via Exact Categories (LB, AC, GR, DSS), pp. 188–198.
LICS-1998-Viswanathan #abstraction #first-order #recursion: Full Abstraction for First-Order Objects with Recursive Types and Subtyping (RV), pp. 380–391.
TLCA-1997-BrandtH #axiom #induction #recursion #similarity: Coinductive Axiomatization of Recursive Type Equality and Subtyping (MB, FH), pp. 63–81.
TLCA-1997-Courant #calculus: A Module Calculus for Pure Type Systems (JC), pp. 112–128.
TLCA-1997-Ghani #calculus #dependent type: Eta-Expansions in Dependent Type Theory — The Calculus of Constructions (NG), pp. 164–180.
ICFP-1997-Banerjee #analysis #composition: A Modular, Polyvariant, and Type-Based Closure Analysis (AB), pp. 1–10.
ICFP-1997-Crary #higher-order #implementation: Foundations for the Implementation of Higher-Order Subtyping (KC), pp. 125–135.
ICFP-1997-MarlowW #erlang: A Practical Subtyping System For Erlang (SM, PW), pp. 136–149.
ECOOP-1997-BrucePF #object-oriented: Subtyping Is Not a Good “Match” for Object-Oriented Languages (KBB, LP, AF), pp. 104–127.
ALP-1997-BartheR #algebra #approach #termination: Termination of Algebraic Type Systems: The Syntactic Approach (GB, FvR), pp. 174–193.
POPL-1997-Rehof: Minimal Typings in Atomic Subtyping (JR), pp. 278–291.
POPL-1997-Saibi #algorithm #inheritance: Typing Algorithm in Type Theory with Inheritance (AS), pp. 292–301.
SAS-1997-Frey #polynomial: Satisfying Subtype Inequalities in Polynomial Space (AF), pp. 265–277.
SAS-1997-IgarashiK #analysis #communication #concurrent #programming language: Type-Based Analysis of Communication for Concurrent Programming Languages (AI, NK), pp. 187–201.
ESEC-FSE-1997-Rushby #specification: Subtypes for Specifications (JMR), pp. 4–19.
TAPSOFT-1997-BonoBDL #constraints: Subtyping Constraints for Incomplete Objects (Extended Abstract) (VB, MB, MDC, LL), pp. 465–477.
TAPSOFT-1997-VolpanoS #approach #security: A Type-Based Approach to Program Security (DMV, GS), pp. 607–621.
CADE-1997-GanzingerMW #order: Soft Typing for Ordered Resolution (HG, CM, CW), pp. 321–335.
LICS-1997-HeintzeM #analysis #on the #polynomial: On the Cubic Bottleneck in Subtyping and Flow Analysis (NH, DAM), pp. 342–351.
LICS-1997-HengleinR #complexity: The Complexity of Subtype Entailment for Simple Types (FH, JR), pp. 352–361.
HT-1996-Allen #automation #hypermedia: Automatic Hypertext Link Typing (JFA), pp. 42–52.
ICALP-1996-MitchellV #effectiveness #modelling #morphism #polymorphism #recursion: Effective Models of Polymorphism, Subtyping and Recursion (JCM, RV), pp. 170–181.
ICFP-1996-Ghelli #complexity #kernel #type checking: Complexity of Kernel Fun Subtype Checking (GG), pp. 134–145.
ICFP-1996-Pottier #constraints: Simplifying Subtyping Constraints (FP), pp. 122–133.
IFL-1996-DebbabiFT #algorithm #analysis #concurrent #control flow #higher-order #source code: A Type-Based Algorithm for the Control-Flow Analysis of Higher-Order Concurrent Programs (MD, AF, NT), pp. 247–266.
ICPR-1996-AokiSAO #prototype #sketching: A prototype system for interpreting hand-sketched floor plans (YA, AS, HA, KO), pp. 747–751.
ECOOP-1996-BrandtK: Generalising the BETA Type System (SB, JLK), pp. 421–448.
ECOOP-1996-GaweckiM #perspective #quantifier: Integrating Subtyping, Matching and Type Quantification: A Practical Perspective (AG, FM), pp. 26–47.
ALP-1996-Nazareth #specification: Specifying Type Systems (DN), pp. 314–329.
POPL-1996-GordonR #calculus #first-order #similarity: Bisimilarity for a First-Order Calculus of Objects with Subtyping (ADG, GDR), pp. 386–395.
SAS-1996-TrifonovS: Subtyping Constrained Types (VT, SFS), pp. 349–365.
FSE-1996-MedvidovicORT #architecture #design #object-oriented #using: Using Object-Oriented Typing to Support Architectural Design in the C2 Style (NM, PO, JER, RNT), pp. 24–32.
ICSE-1996-DharaL #behaviour #inheritance #specification: Forcing Behavioral Subtyping through Specification Inheritance (KKD, GTL), pp. 258–267.
ESOP-1996-SmithV #c #polymorphism #towards: Towards an ML-Style Polymorphic Type System for C (GS, DMV), pp. 341–355.
CSL-1996-BartheM #algebra #on the #reduction: On the Subject Reduction Property for Algebraic Type Systems (GB, PAM), pp. 34–57.
CSL-1996-Geuvers #dependent type #higher-order #logic #modelling: Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory (HG), pp. 167–181.
CSL-1996-Luo: Coercive Subtyping in Type Theory (ZL), pp. 276–296.
LICS-1996-AspinallC #dependent type: Subtyping Dependent Types (DA, ABC), pp. 86–97.
LICS-1996-TiurynU #decidability #higher-order #problem: The Subtyping Problem for Second-Order Types is Undecidable (JT, PU), pp. 74–85.
RTA-1995-BakelF #normalisation #term rewriting: (Head-) Normalization of Typeable Rewrite Systems (SvB, MF), pp. 279–293.
TLCA-1995-Barthe: Extensions of Pure Type Systems (GB), pp. 16–31.
TLCA-1995-BerardiB #optimisation #using: Using Subtyping in Program Optimization (SB, LB), pp. 63–77.
TLCA-1995-Holmes #λ-calculus: Untyped λ-Calculus with Relative Typing (MRH), pp. 235–248.
TLCA-1995-KurataT #decidability: Decidable Properties of Intersection Type Systems (TK, MT), pp. 297–311.
FPCA-1995-AikenF #dynamic typing #type inference: Dynamic Typing and Subtype Inference (AA, MF), pp. 182–191.
FPCA-1995-Thiemann #polymorphism #revisited: Unboxed Values and Polymorphic Typing Revisited (PT), pp. 24–35.
ECOOP-1995-AbadiC #on the: On Subtyping and Matching (MA, LC), pp. 145–167.
OOPSLA-1995-DayGLM #morphism #parametricity #polymorphism: Subtypes vs. Where Clauses: Constraining Parametric Polymorphism (MD, RG, BL, ACM), pp. 156–168.
PEPM-1995-TangJ: Effect Systems with Subtyping (YMT, PJ), pp. 45–53.
PLDI-1995-ShaoA #compilation #ml #standard: A Type-Based Compiler for Standard ML (ZS, AWA), pp. 116–129.
POPL-1995-HoangM #bound #type inference: Lower Bounds on Type Inference with Subtypes (MH, JCM), pp. 176–185.
POPL-1995-HofmannP: Positive Subtyping (MH, BCP), pp. 186–197.
POPL-1995-PalsbergO #analysis: A Type System Equivalent to Flow Analysis (JP, PO), pp. 367–378.
SAS-1995-DussartHM #analysis #polymorphism #polynomial #recursion: Polymorphic Recursion and Subtype Qualifications: Polymorphic Binding-Time Analysis in Polynomial Time (DD, FH, CM), pp. 118–135.
SAS-1995-Hannan #analysis #functional #stack: A Type-based Analysis for Stack Allocation in Functional Languages (JH), pp. 172–188.
SAS-1995-Heintze #analysis #control flow: Control-Flow Analysis and Type Systems (NH), pp. 189–206.
KBSE-1995-Reuss #deduction #synthesis #towards: Towards High-Level Deductive Program Synthesis Based on Type Theory (HR), pp. 174–183.
LICS-1995-Constable #experience: Experience with Type Theory as a Foundation for Computer Science (RLC), pp. 266–279.
LICS-1995-LongoMS #logic: A Logic of Subtyping (GL, KM, SS), pp. 292–299.
LFP-1994-WrightC: A Practical Soft Type System for Scheme (AKW, RC), pp. 250–262.
ECOOP-1994-AlagicSB #declarative #inheritance #object-oriented #programming #prototype: Declarative Object-Oriented Programming: Inheritance, Subtyping and Prototyping (SA, RS, RB), pp. 236–259.
OOPSLA-1994-EifrigSTZ #decidability #object-oriented: Application of OOP Type Theory: State, Decidability, Integragtion (JE, SFS, VT, AEZ), pp. 16–30.
PEPM-1994-Baker-Finch #higher-order #static analysis: Type Theory and Projections for Higher-Order Static Analysis (CABF), pp. 43–52.
POPL-1994-AikenWL: Soft Typing with Conditional Types (AA, ELW, TKL), pp. 163–173.
POPL-1994-KatiyarLM #prototype: A Type System for Prototyping Languages (DK, DCL, JCM), pp. 138–150.
SAS-1994-HankinM #framework #program analysis: A Type-based Framework for Program Analysis (CH, DLM), pp. 380–394.
SAS-1994-Henglein #analysis #fixpoint #strict: Iterative Fixed Point Computation for Type-Based Strictness Analysis (FH), pp. 395–407.
ESOP-J-1992-Henglein94 #dynamic typing #proving #syntax: Dynamic Typing: Syntax and Proof Theory (FH), pp. 197–230.
CADE-1994-Jackson #algebra: Exploring Abstract Algebra in Constructive Type Theory (PJ), pp. 590–604.
LICS-1994-GeuversW #on the: On the Church-Rosser Property for Expressive Type Systems and its Consequences for their Metatheoretic Study (HG, BW), pp. 320–329.
LICS-1994-PlotkinAC #parametricity: Subtyping and Parametricity (GDP, MA, LC), pp. 310–319.
SIGMOD-1993-BukhresCELM #multi #named #prototype: InterBase: A Multidatabase Prototype System (OAB, JC, AKE, XL, JGM), pp. 534–539.
WCRE-1993-OlshefskiC #comprehension #prototype: A Prototype System for static and Dynamic Program Understanding (DO, AC), pp. 93–106.
TLCA-1993-JacobsM #dependent type #higher-order #logic: Translating Dependent Type Theory into Higher Order Logic (BJ, TFM), pp. 209–229.
TLCA-1993-McKinnaP: Pure Type Systems Formalized (JM, RP), pp. 289–305.
FPCA-1993-Lillie: Conjunctive Subtyping (DJL), pp. 42–51.
HCI-ACS-1993-KanSH #evaluation #towards: Toward a Cognitive Ergonomics Evaluation System of Typing Chinese Characters into Computers (ZK, GS, ZH), pp. 380–385.
ECOOP-1993-LiskovW: A New Definition of the Subtype Relation (BL, JMW), pp. 118–141.
OOPSLA-1993-Lamping #interface: Typing the Specialization Interface (JL), pp. 201–214.
OOPSLA-1993-LiskovW #specification: Specifications and Their Use in Defining Subtypes (BL, JMW), pp. 16–28.
POPL-1993-Aponte #parametricity: Extending Record Typing to Type Parametric Modules with Sharing (MVA), pp. 465–478.
POPL-1993-KozenPS #performance #recursion: Efficient Recursive Subtyping (DK, JP, MIS), pp. 419–428.
POPL-1993-Mairson #logic #multi: A Constructive Logic of Multiple Subtyping (HGM), pp. 313–324.
TAPSOFT-1993-Mahr: Applications of Type Theory (BM), pp. 343–355.
TAPSOFT-1993-Smith #polymorphism #type inference: Polymorphic Type Inference with Overloading and Subtyping (GS), pp. 671–685.
TAPSOFT-1993-TiurynW #re-engineering #recursion: Type Reconstruction with Recursive Types and Atomic Subtyping (JT, MW), pp. 686–701.
ILPS-1993-MoraPRF #equation #prototype: A Prototype System for Equational Constructive Negation (AM, JP, MJR, MF), p. 638.
LFP-1992-CastagnaGL #calculus: A Calculus for Overloaded Functions with Subtyping (GC, GG, GL), pp. 182–192.
LFP-1992-Kaes #recursion #type inference: Type Inference in the Presence of Overloading, Subtyping and Recursive Types (SK), pp. 193–204.
SEKE-1992-SubramaniamTHRR #design #information management #prototype: Knowledge Engineering for Protein Structure and Motifs: Design of a Prototype System (SS, DKT, KH, HR, LAR), pp. 420–435.
ECOOP-1992-DodaniT #named #object-oriented #programming: ACTS: A Type System for Object-Oriented Programming Based on Abstract and Concrete Classes (MD, CST), pp. 309–328.
TOOLS-USA-1992-Alagic #object-oriented: Object-Oriented Type Systems (SA), p. 295.
POPL-1992-BruceM #higher-order #modelling #morphism #polymorphism #recursion: PER Models of Subtyping, Recursive Types and Higher-Order Polymorphism (KBB, JCM), pp. 316–327.
POPL-1992-Leroy #polymorphism: Unboxed Objects and Polymorphic Typing (XL), pp. 177–188.
POPL-1992-LincolnM #algorithm #aspect-oriented #type inference: Algorithmic Aspects of Type Inference with Subtypes (PL, JCM), pp. 293–304.
POPL-1992-Ma #parametricity: Parametricity as Subtyping (QM), pp. 281–292.
POPL-1992-Remy #for free: Typing Record Concatenation for Free (DR), pp. 166–176.
ESOP-1992-DohS #action semantics #semantics: Extraction of Strong Typing Laws from Action Semantics Definitions (KGD, DAS), pp. 151–166.
ESOP-1992-Henglein #dynamic typing: Dynamic Typing (FH), pp. 233–253.
ESOP-1992-Wright: Typing References by Effect Inference (AKW), pp. 473–491.
CADE-1992-NipkowQ #reduction #unification #λ-calculus: Reduction and Unification in Lambda Calculi with Subtypes (TN, ZQ), pp. 66–78.
CSL-1992-Smith: Kleene’s Slash and Existence of Values of Open Terms in Type Theory (JMS), pp. 395–402.
JICSLP-1992-RouzaudN #prolog: Integrating Modes and Subtypes into a Prolog Type-Checker (YR, LNP), pp. 85–97.
LICS-1992-Tiuryn: Subtype Inequalities (JT), pp. 308–315.
PODS-1991-BeeriM: Subtyping in OODB’s (CB, TM), pp. 300–314.
OOPSLA-1991-Ghelli #message passing #static typing: A Static Type System for Message Passing (GG), pp. 129–145.
PLDI-1991-CartwrightF: Soft Typing (RC, MF), pp. 278–292.
POPL-1991-AmadioC #recursion: Subtyping Recursive Types (RMA, LC), pp. 104–118.
POPL-1991-DubaHM #continuation #ml: Typing First-Class Continuations in ML (BFD, RH, DBM), pp. 163–173.
POPL-1991-MitchellMM #inheritance #ml #standard: An Extension of Standard ML Modules with Subtyping and Inheritance (JCM, SM, NM), pp. 270–278.
Best-of-PLDI-1991-CartwrightF91a: Soft typing (with retrospective) (RC, MF), pp. 412–428.
ESEC-1991-Parisi-PresicceP #algebra #inheritance #object-oriented #programming: An Algebraic View of Inheritance and Subtyping in Object Oriented Programming (FPP, AP), pp. 364–379.
ESOP-J-1990-Helmink91: Resolution and Type Theory (LH), pp. 119–138.
ESOP-J-1990-Thatte91 #scalability: A Type System for Implicit Scaling (ST), pp. 217–245.
CAAP-1991-Luo #refinement #specification: Program Specification and Data Refinement in Type Theory (ZL), pp. 143–168.
ISLP-1991-LakshmanR #prolog #re-engineering #semantics: Typed Prolog: A Semantic Reconstruction of the Mycroft-O’Keefe Type System (TLL, USR), pp. 202–217.
LICS-1991-Howe #on the: On Computational Open-Endedness in Martin-Löf’s Type Theory (DJH), pp. 162–172.
OOPSLA-ECOOP-1990-AmericaL #inheritance #object-oriented #parallel: A Parallel Object-Oriented Language with Inheritance and Subtyping (PA, FvdL), pp. 161–168.
OOPSLA-ECOOP-1990-LeavensW #object-oriented #reasoning #source code: Reasoning about Object-Oriented Programs that Use Subtypes (GTL, WEW), pp. 212–223.
OOPSLA-ECOOP-1990-MadsenMM #object-oriented #revisited: Strong Typing of Object-Oriented Languages Revisited (OLM, BM, BMP), pp. 140–150.
PLDI-1990-Jacobs #constraints #logic programming: Type Declarations as Subtype Constraints in Logic Programming (DJ), pp. 165–173.
POPL-1990-CookHC #inheritance: Inheritance Is Not Subtyping (WRC, WLH, PSC), pp. 125–135.
POPL-1990-GraverJ #smalltalk: A Type System for Smalltalk (JOG, REJ), pp. 136–150.
POPL-1990-Griffin: A Formulae-as-Types Notion of Control (TG), pp. 47–58.
POPL-1990-Thatte #static typing: Quasi-Static Typing (SRT), pp. 367–381.
ESOP-1990-Helmink: Resolution and Type Theory (LH), pp. 197–211.
PODS-1989-Borgida #inheritance #query #strict: Type Systems for Querying Class Hierarchies with Non-strict Inheritance (AB), pp. 394–400.
CHI-1989-JohnN #human-computer: Cumulating the science of HCI: from s-R compatibility to transcription typing (BEJ, AN), pp. 109–114.
POPL-1989-AbadiCPP #dynamic typing #static typing: Dynamic Typing in a Statically-Typed Language (MA, LC, BCP, GDP), pp. 213–227.
POPL-1989-CardelliDJKN: The Modula-3 Type System (LC, JED, MJJ, BK, GN), pp. 202–212.
POPL-1989-KanellakisM #ml #polymorphism #unification: Polymorphic Unification and ML Typing (PCK, JCM), pp. 105–115.
POPL-1989-YelickZ #logic programming: Moded Type Systems for Logic Programming (KAY, JLZ), pp. 116–124.
CCIPL-1989-FuhM #polymorphism #type inference: Polymorphic Subtype Inference: Closing the Theory-Practice Gap (YCF, PM), pp. 167–183.
LICS-1989-Pitts #polymorphism: Non-trivial Power Types Can’t Be Subtypes of Polymorphic Types (AMP), pp. 6–13.
LFP-1988-JategaonkarM #ml #pattern matching: ML with Extended Pattern Matching and Subtypes (LJ, JCM), pp. 198–211.
PLDI-1988-Rose #design: Refined Types: Highly Differentiated Type Systems and Their Use in the Design of Intermediate Langages (JRR), pp. 278–287.
POPL-1988-Cardelli: Structural Subtyping and the Notion of Power Type (LC), pp. 70–79.
POPL-1988-Stansifer #type inference: Type Inference with Subtypes (RS), pp. 88–97.
ESOP-1988-DietrichH #polymorphism #prolog: A Polymorphic Type System with Subtypes for Prolog (RD, FH), pp. 79–93.
ESOP-1988-FuhM #type inference: Type Inference with Subtypes (YCF, PM), pp. 94–114.
ESOP-1988-Parigot #higher-order #programming #proving: Programming with Proofs: A Second Order Type Theory (MP), pp. 145–159.
CADE-1988-Jacquet #synthesis: Program Synthesis by Completion with Dependent Subtypes (PJ), pp. 550–562.
LICS-1988-SalvesenS #set: The Strength of the Subset Type in Martin-Löf’s Type Theory (AS, JMS), pp. 384–391.
ECOOP-1987-America #inheritance #object-oriented #parallel: Inheritance and Subtyping in a Parallel Object-Oriented Language (PA), pp. 234–242.
LICS-1987-ConstableS: Partial Objects In Constructive Type Theory (RLC, SFS), pp. 183–193.
OOPSLA-1986-Olthoff #concept #data type #experience #object-oriented #programming: Augmentation of Object-Oriented Programming by Concepts of Abstract Data Type Theory: The ModPascal Experience (WGO), pp. 429–443.
LICS-1986-KnoblockC: Formalized Metareasoning in Type Theory (TBK, RLC), pp. 237–248.
LICS-1986-MendlerPC #infinity: Infinite Objects in Type Theory (NPM, PP, RLC), pp. 249–255.
POPL-1985-LamportS #alias #approach #constraints #named: Constraints: A Uniform Approach to Aliasing and Typing (LL, FBS), pp. 205–216.
POPL-1983-Kieburtz #data type #precise #specification: Precise Typing of Abstract Data Type Specifications (RBK), pp. 109–116.
DAC-1983-KowalskiT #automation #design #prototype: The VLSI Design Automation Assistant: Prototype system (TJK, DET), pp. 479–483.
VLDB-1978-Palmer #database: Record Subtype Facilities in Database Systems (IRP), pp. 148–155.