Tag #dependent type
89 papers:
POPL-2020-ChangBTB #metaprogramming #type system- Dependent type systems as macros (SC, MB, MT, WJB), p. 29.
- POPL-2020-MackayPAG #decidability #type system
- Decidable subtyping for path dependent types (JM, AP, JA, LG), p. 27.
FSCD-2019-BlanquiGH #dependence #modulo theories #termination #type system- Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting (FB, GG, OH), p. 21.
- ICFP-2019-EremondiTG #approximate #normalisation
- Approximate normalization for gradual dependent types (JE, ÉT, RG), p. 30.
- ICFP-2019-GratzerSB #implementation #type system
- Implementing a modal dependent type theory (DG, JS, LB), p. 29.
- ICFP-2019-WeirichCVE #haskell
- A role for dependent types in Haskell (SW, PC, AV, RAE), p. 29.
OOPSLA-2019-RapoportL #formal method- A path to DOT: formalizing fully path-dependent types (MR, OL), p. 29.
- ICFP-2018-CongA #continuation
- Handling delimited continuations with dependent types (YC, KA), p. 31.
- ICFP-2018-DiehlFS #low cost #reuse
- Generic zero-cost reuse for dependent types (LD, DF, AS), p. 30.
ECOOP-2018-CamposV - Dependent Types for Class-based Mutable Objects (JC, VTV), p. 28.
- ICFP-2017-0001VW #evaluation #normalisation
- Normalization by evaluation for sized dependent types (AA0, AV, TW), p. 30.
- ICFP-2017-NuytsVD #parametricity #quantifier #type system
- Parametric quantifiers for dependent type theory (AN, AV, DD), p. 29.
- ICFP-2017-WeirichVAE #haskell #specification
- A specification for dependent types in Haskell (SW, AV, PHAdA, RAE), p. 29.
- POPL-2017-Weirich
- The influence of dependent types (keynote) (SW), p. 1.
ESOP-2017-Miquey #calculus- A Classical Sequent Calculus with Dependent Types (ÉM), pp. 777–803.
- FSCD-2016-AltenkirchK #evaluation #normalisation
- Normalisation by Evaluation for Dependent Types (TA, AK), p. 16.
- POPL-2016-SwamyHKRDFBFSKZ #multi
- Dependent types and multi-monadic effects in F (NS, CH, CK, AR, ADL, SF, KB, CF, PYS, MK, JKZ, SZB), pp. 256–270.
ICALP-v2-2015-AbramskyJV #game studies- Games for Dependent Types (SA, RJ, MV), pp. 31–43.
TLCA-2015-FairweatherFST - Dependent Types for Nominal Terms with Atom Substitutions (EF, MF, NS, AT), pp. 180–195.
- POPL-2015-KrishnaswamiPB #linear
- Integrating Linear and Dependent Types (NRK, PP, NB), pp. 17–30.
BX-2014-GrohneLV #bidirectional #formal method #semantics- Formalizing Semantic Bidirectionalization with Dependent Types (HG, AL, JV), pp. 75–81.
- OOPSLA-2014-AminRO
- Foundations of path-dependent types (NA, TR, MO), pp. 233–249.
PPDP-J-2012-LagoP14 #call-by #linear- Linear dependent types in a call-by-value scenario (UDL, BP), pp. 77–100.
- POPL-2014-AtkeyGJ #parametricity #type system
- A relationally parametric model of dependent type theory (RA, NG, PJ), pp. 503–516.
CEFP-2013-Brady #domain-specific language #embedded #implementation #programming language- The Idris Programming Language — Implementing Embedded Domain Specific Languages with Dependent Types (EB), pp. 115–186.
ICFP-2013-Brady #algebra #programming #reasoning- Programming and reasoning with algebraic effects and dependent types (EB), pp. 133–144.
- ICFP-2013-Norell #interactive #programming
- Interactive programming with dependent types (UN), pp. 1–2.
IFL-2013-FowlerB #programming #web- Dependent Types for Safe and Secure Web Programming (SF, EB), p. 49.
- POPL-2013-GaboardiHHNP #difference #linear #privacy
- Linear dependent types for differential privacy (MG, AH, JH, AN, BCP), pp. 357–370.
- PPDP-2013-StewartBN #data flow #data type #policy #semistructured data
- Dependent types for enforcement of information flow and erasure policies in heterogeneous data structures (GS, AB, AN), pp. 145–156.
VMCAI-2013-ZhuJ #composition #lightweight #ml #type inference- Compositional and Lightweight Dependent Type Inference for ML (HZ, SJ), pp. 295–314.
- ICFP-2012-McBride #programming
- Agda-curious?: an exploration of programming with dependent types (CTM), pp. 1–2.
- OOPSLA-2012-ChughHJ #javascript
- Dependent types for JavaScript (RC, DH, RJ), pp. 587–606.
- PPDP-2012-LagoP #call-by #linear
- Linear dependent types in a call-by-value scenario (UDL, BP), pp. 115–126.
- TLCA-2011-AbelP #higher-order #unification
- Higher-Order Dynamic Pattern Unification for Dependent Types and Records (AA, BP), pp. 10–26.
- TLCA-2011-SvendsenBN
- Partiality, State and Dependent Types (KS, LB, AN), pp. 198–212.
- ICFP-2011-SwamyCFSBY #distributed #programming
- Secure distributed programming with value-dependent types (NS, JC, CF, PYS, KB, JY), pp. 266–278.
- POPL-2011-RamseyD #composition #independence #low level #type system #using
- Resourceable, retargetable, modular instruction selection using a machine-independent, type-based tiling of low-level intermediate code (NR, JD), pp. 575–586.
LICS-2011-LagoG #linear- Linear Dependent Types and Relative Completeness (UDL, MG), pp. 133–142.
FLOPS-2010-AltenkirchDLO #named- ΠΣ: Dependent Types without the Sugar (TA, NAD, AL, NO), pp. 40–55.
- FLOPS-2010-Pientka #named #programming
- Beluga: Programming with Dependent Types, Contextual Data, and Contexts (BP), pp. 1–12.
- ICFP-2010-BernardyJP #parametricity
- Parametricity and dependent types (JPB, PJ, RP), pp. 345–356.
- POPL-2010-JiaZSW #equivalence
- Dependent types and program equivalence (LJ, JZ, VS, SW), pp. 275–286.
- POPL-2010-Terauchi
- Dependent types from counterexamples (TT), pp. 119–130.
- ICFP-2009-SculthorpeN #functional #programming
- Safe functional reactive programming through dependent types (NS, HN), pp. 23–34.
PEPM-2009-SalamaMTGO #consistency #using- Static consistency checking for verilog wire interconnects: using dependent types to check the sanity of verilog descriptions (CS, GM, WT, JG, JO), pp. 121–130.
- PPDP-2009-UnnoK #type inference
- Dependent type inference with interpolants (HU, NK), pp. 277–288.
- FLOPS-2008-UnnoK #on-demand #refinement
- On-Demand Refinement of Dependent Types (HU, NK), pp. 81–96.
- ICFP-2008-NanevskiMSGB #imperative #named #source code
- Ynot: dependent types for imperative programs (AN, GM, AS, PG, LB), pp. 229–240.
- IFL-2008-TrojahnerG #array #representation
- Descriptor-Free Representation of Arrays with Dependent Types (KT, CG), pp. 100–117.
- ESOP-2008-PoswolskyS #encoding #higher-order #programming
- Practical Programming with Higher-Order Encodings and Dependent Types (AP, CS), pp. 93–107.
FoSSaCS-2008-BarrasB #calculus #programming language- The Implicit Calculus of Constructions as a Programming Language with Dependent Types (BB, BB), pp. 365–379.
- IFL-2007-HerhutSBGT #contract #partial evaluation #proving #towards
- From Contracts Towards Dependent Types: Proofs by Partial Evaluation (SH, SBS, RB, CG, KT), pp. 254–273.
- IFL-2007-Kleeblatt #using
- Checking Dependent Types Using Compiled Code (DK), pp. 165–182.
WRLA-J-2004-CervesatoS07 #logic #representation #specification- Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types (IC, MOS), pp. 3–35.
- ESOP-2007-ConditHAGN #low level #programming
- Dependent Types for Low-Level Programming (JC, MH, ZRA, DG, GCN), pp. 520–535.
- POPL-2006-McKinna #matter #why
- Why dependent types matter (JM), p. 1.
CC-2006-Necula #low level #type system #using- Using Dependent Types to Port Type Systems to Low-Level Languages (GCN), p. 1.
IJCAR-2006-Rabe #first-order #logic- First-Order Logic with Dependent Types (FR), pp. 377–391.
SAS-2005-HarrenN #assembly #safety #using- Using Dependent Types to Certify the Safety of Assembly Code (MH, GCN), pp. 155–170.
- WRLA-2004-CervesatoS05 #logic #representation #specification
- Representing the MSR Cryptoprotocol Specification Language in an Extension of Rewriting Logic with Dependent Types (IC, MOS), pp. 183–207.
TACAS-2005-KomondoorRCF #comprehension- Dependent Types for Program Understanding (RK, GR, SC, JF), pp. 157–173.
AFP-2004-McBride04 #named #programming- Epigram: Practical Programming with Dependent Types (CM), pp. 130–170.
PADL-2004-ChenZX #case study #haskell #implementation #simulation- Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell (CC, DZ, HX), pp. 239–254.
- POPL-2004-Yoshida #higher-order #mobile #process
- Channel dependent types for higher-order mobile processes (NY), pp. 147–160.
CSL-2004-SchoppS #type system- A Dependent Type Theory with Names and Binding (US, IS), pp. 235–249.
SEFM-2003-Xi #verification- Facilitating Program Verification with Dependent Types (HX), pp. 72–81.
- ECOOP-2003-OderskyCRZ
- A Nominal Theory of Objects with Dependent Types (MO, VC, CR, MZ), pp. 201–224.
- TLCA-2001-Danner
- Ramified Recurrence with Dependent Types (ND), pp. 91–105.
- TLCA-2001-Geuvers #higher-order #induction #type system
- Induction Is Not Derivable in Second Order Dependent Type Theory (HG), pp. 166–181.
- FoSSaCS-2001-BartheP #morphism #proving #reuse #type system
- Type Isomorphisms and Proof Reuse in Dependent Type Theory (GB, OP), pp. 57–71.
- LICS-2001-Xi #termination #verification
- Dependent Types for Program Termination Verification (HX), pp. 231–242.
- CSL-2000-BauerB
- Continuous Functionals of Dependent Types and Equilogical Spaces (AB, LB), pp. 202–216.
- CSL-2000-HancockS #interactive #source code #type system
- Interactive Programs in Dependent Type Theory (PH, AS), pp. 317–331.
- LICS-2000-Xi #imperative #programming
- Imperative Programming with Dependent Types (HX), pp. 375–387.
- PADL-1999-Xi
- Dead Code Elimination through Dependent Types (HX), pp. 228–242.
- POPL-1999-XiP #programming
- Dependent Types in Practical Programming (HX, FP), pp. 214–227.
- PPDP-1999-Russo #ml #standard
- Non-dependent Types for Standard ML Modules (CVR), pp. 80–97.
- AFP-1998-Augustsson98 #named
- Cayenne — A Language with Dependent Types (LA), pp. 240–267.
- ICFP-1998-Augustsson #named
- Cayenne — a Language with Dependent Types (LA), pp. 239–250.
PLDI-1998-XiP #array #bound- Eliminating Array Bound Checking Through Dependent Types (HX, FP), pp. 249–257.
- TLCA-1997-Ghani #calculus #type system
- Eta-Expansions in Dependent Type Theory — The Calculus of Constructions (NG), pp. 164–180.
RTA-1996-Virga #higher-order- Higher-Order Superposition for Dependent Types (RV), pp. 123–137.
- CSL-1996-Geuvers #higher-order #logic #modelling #type system
- Extending Models of Second Order Predicate Logic to Models of Second Dependent Type Theory (HG), pp. 167–181.
- LICS-1996-AspinallC #type system
- Subtyping Dependent Types (DA, ABC), pp. 86–97.
- TLCA-1993-JacobsM #higher-order #logic #type system
- Translating Dependent Type Theory into Higher Order Logic (BJ, TFM), pp. 209–229.
CCPSD-1991-Krieg-BrucknerS #higher-order #in the large #in the small #inheritance #specification- Structuring Specifications in-the-Large and in-the-Small: Higher-Order Functions, Dependent Types and Inheritance in SPECTRAL (BKB, DS), pp. 313–336.
LFP-1990-SheldonG - Static Dependent Types for First Class Modules (MAS, DKG), pp. 20–29.
- POPL-1986-MacQueen #composition #using
- Using Dependent Types to Express Modular Structure (DBM), pp. 277–286.
