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
type system
Google type system

Tag #type system

663 papers:

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

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.