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

Tag #dependent type

89 papers:

POPLPOPL-2020-ChangBTB #metaprogramming #type system
Dependent type systems as macros (SC, MB, MT, WJB), p. 29.
POPLPOPL-2020-MackayPAG #decidability #type system
Decidable subtyping for path dependent types (JM, AP, JA, LG), p. 27.
FSCDFSCD-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.
OOPSLAOOPSLA-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.
ECOOPECOOP-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.
POPLPOPL-2017-Weirich
The influence of dependent types (keynote) (SW), p. 1.
ESOPESOP-2017-Miquey #calculus
A Classical Sequent Calculus with Dependent Types (ÉM), pp. 777–803.
FSCDFSCD-2016-AltenkirchK #evaluation #normalisation
Normalisation by Evaluation for Dependent Types (TA, AK), p. 16.
POPLPOPL-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.
ICALPICALP-v2-2015-AbramskyJV #game studies
Games for Dependent Types (SA, RJ, MV), pp. 31–43.
TLCATLCA-2015-FairweatherFST
Dependent Types for Nominal Terms with Atom Substitutions (EF, MF, NS, AT), pp. 180–195.
POPLPOPL-2015-KrishnaswamiPB #linear
Integrating Linear and Dependent Types (NRK, PP, NB), pp. 17–30.
BXBX-2014-GrohneLV #bidirectional #formal method #semantics
Formalizing Semantic Bidirectionalization with Dependent Types (HG, AL, JV), pp. 75–81.
OOPSLAOOPSLA-2014-AminRO
Foundations of path-dependent types (NA, TR, MO), pp. 233–249.
PPDPPPDP-J-2012-LagoP14 #call-by #linear
Linear dependent types in a call-by-value scenario (UDL, BP), pp. 77–100.
POPLPOPL-2014-AtkeyGJ #parametricity #type system
A relationally parametric model of dependent type theory (RA, NG, PJ), pp. 503–516.
CEFPCEFP-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.
ICFPICFP-2013-Brady #algebra #programming #reasoning
Programming and reasoning with algebraic effects and dependent types (EB), pp. 133–144.
ICFPICFP-2013-Norell #interactive #programming
Interactive programming with dependent types (UN), pp. 1–2.
IFLIFL-2013-FowlerB #programming #web
Dependent Types for Safe and Secure Web Programming (SF, EB), p. 49.
POPLPOPL-2013-GaboardiHHNP #difference #linear #privacy
Linear dependent types for differential privacy (MG, AH, JH, AN, BCP), pp. 357–370.
PPDPPPDP-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.
VMCAIVMCAI-2013-ZhuJ #composition #lightweight #ml #type inference
Compositional and Lightweight Dependent Type Inference for ML (HZ, SJ), pp. 295–314.
ICFPICFP-2012-McBride #programming
Agda-curious?: an exploration of programming with dependent types (CTM), pp. 1–2.
OOPSLAOOPSLA-2012-ChughHJ #javascript
Dependent types for JavaScript (RC, DH, RJ), pp. 587–606.
PPDPPPDP-2012-LagoP #call-by #linear
Linear dependent types in a call-by-value scenario (UDL, BP), pp. 115–126.
TLCATLCA-2011-AbelP #higher-order #unification
Higher-Order Dynamic Pattern Unification for Dependent Types and Records (AA, BP), pp. 10–26.
TLCATLCA-2011-SvendsenBN
Partiality, State and Dependent Types (KS, LB, AN), pp. 198–212.
ICFPICFP-2011-SwamyCFSBY #distributed #programming
Secure distributed programming with value-dependent types (NS, JC, CF, PYS, KB, JY), pp. 266–278.
POPLPOPL-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.
LICSLICS-2011-LagoG #linear
Linear Dependent Types and Relative Completeness (UDL, MG), pp. 133–142.
FLOPSFLOPS-2010-AltenkirchDLO #named
ΠΣ: Dependent Types without the Sugar (TA, NAD, AL, NO), pp. 40–55.
FLOPSFLOPS-2010-Pientka #named #programming
Beluga: Programming with Dependent Types, Contextual Data, and Contexts (BP), pp. 1–12.
ICFPICFP-2010-BernardyJP #parametricity
Parametricity and dependent types (JPB, PJ, RP), pp. 345–356.
POPLPOPL-2010-JiaZSW #equivalence
Dependent types and program equivalence (LJ, JZ, VS, SW), pp. 275–286.
POPLPOPL-2010-Terauchi
Dependent types from counterexamples (TT), pp. 119–130.
ICFPICFP-2009-SculthorpeN #functional #programming
Safe functional reactive programming through dependent types (NS, HN), pp. 23–34.
PEPMPEPM-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.
PPDPPPDP-2009-UnnoK #type inference
Dependent type inference with interpolants (HU, NK), pp. 277–288.
FLOPSFLOPS-2008-UnnoK #on-demand #refinement
On-Demand Refinement of Dependent Types (HU, NK), pp. 81–96.
ICFPICFP-2008-NanevskiMSGB #imperative #named #source code
Ynot: dependent types for imperative programs (AN, GM, AS, PG, LB), pp. 229–240.
IFLIFL-2008-TrojahnerG #array #representation
Descriptor-Free Representation of Arrays with Dependent Types (KT, CG), pp. 100–117.
ESOPESOP-2008-PoswolskyS #encoding #higher-order #programming
Practical Programming with Higher-Order Encodings and Dependent Types (AP, CS), pp. 93–107.
FoSSaCSFoSSaCS-2008-BarrasB #calculus #programming language
The Implicit Calculus of Constructions as a Programming Language with Dependent Types (BB, BB), pp. 365–379.
IFLIFL-2007-HerhutSBGT #contract #partial evaluation #proving #towards
From Contracts Towards Dependent Types: Proofs by Partial Evaluation (SH, SBS, RB, CG, KT), pp. 254–273.
IFLIFL-2007-Kleeblatt #using
Checking Dependent Types Using Compiled Code (DK), pp. 165–182.
WRLAWRLA-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.
ESOPESOP-2007-ConditHAGN #low level #programming
Dependent Types for Low-Level Programming (JC, MH, ZRA, DG, GCN), pp. 520–535.
POPLPOPL-2006-McKinna #matter #why
Why dependent types matter (JM), p. 1.
CCCC-2006-Necula #low level #type system #using
Using Dependent Types to Port Type Systems to Low-Level Languages (GCN), p. 1.
IJCARIJCAR-2006-Rabe #first-order #logic
First-Order Logic with Dependent Types (FR), pp. 377–391.
SASSAS-2005-HarrenN #assembly #safety #using
Using Dependent Types to Certify the Safety of Assembly Code (MH, GCN), pp. 155–170.
WRLAWRLA-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.
TACASTACAS-2005-KomondoorRCF #comprehension
Dependent Types for Program Understanding (RK, GR, SC, JF), pp. 157–173.
AFPAFP-2004-McBride04 #named #programming
Epigram: Practical Programming with Dependent Types (CM), pp. 130–170.
PADLPADL-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.
POPLPOPL-2004-Yoshida #higher-order #mobile #process
Channel dependent types for higher-order mobile processes (NY), pp. 147–160.
CSLCSL-2004-SchoppS #type system
A Dependent Type Theory with Names and Binding (US, IS), pp. 235–249.
SEFMSEFM-2003-Xi #verification
Facilitating Program Verification with Dependent Types (HX), pp. 72–81.
ECOOPECOOP-2003-OderskyCRZ
A Nominal Theory of Objects with Dependent Types (MO, VC, CR, MZ), pp. 201–224.
TLCATLCA-2001-Danner
Ramified Recurrence with Dependent Types (ND), pp. 91–105.
TLCATLCA-2001-Geuvers #higher-order #induction #type system
Induction Is Not Derivable in Second Order Dependent Type Theory (HG), pp. 166–181.
FoSSaCSFoSSaCS-2001-BartheP #morphism #proving #reuse #type system
Type Isomorphisms and Proof Reuse in Dependent Type Theory (GB, OP), pp. 57–71.
LICSLICS-2001-Xi #termination #verification
Dependent Types for Program Termination Verification (HX), pp. 231–242.
CSLCSL-2000-BauerB
Continuous Functionals of Dependent Types and Equilogical Spaces (AB, LB), pp. 202–216.
CSLCSL-2000-HancockS #interactive #source code #type system
Interactive Programs in Dependent Type Theory (PH, AS), pp. 317–331.
LICSLICS-2000-Xi #imperative #programming
Imperative Programming with Dependent Types (HX), pp. 375–387.
PADLPADL-1999-Xi
Dead Code Elimination through Dependent Types (HX), pp. 228–242.
POPLPOPL-1999-XiP #programming
Dependent Types in Practical Programming (HX, FP), pp. 214–227.
PPDPPPDP-1999-Russo #ml #standard
Non-dependent Types for Standard ML Modules (CVR), pp. 80–97.
AFPAFP-1998-Augustsson98 #named
Cayenne — A Language with Dependent Types (LA), pp. 240–267.
ICFPICFP-1998-Augustsson #named
Cayenne — a Language with Dependent Types (LA), pp. 239–250.
PLDIPLDI-1998-XiP #array #bound
Eliminating Array Bound Checking Through Dependent Types (HX, FP), pp. 249–257.
TLCATLCA-1997-Ghani #calculus #type system
Eta-Expansions in Dependent Type Theory — The Calculus of Constructions (NG), pp. 164–180.
RTARTA-1996-Virga #higher-order
Higher-Order Superposition for Dependent Types (RV), pp. 123–137.
CSLCSL-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.
LICSLICS-1996-AspinallC #type system
Subtyping Dependent Types (DA, ABC), pp. 86–97.
TLCATLCA-1993-JacobsM #higher-order #logic #type system
Translating Dependent Type Theory into Higher Order Logic (BJ, TFM), pp. 209–229.
TAPSOFTCCPSD-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.
LISPLFP-1990-SheldonG
Static Dependent Types for First Class Modules (MAS, DKG), pp. 20–29.
POPLPOPL-1986-MacQueen #composition #using
Using Dependent Types to Express Modular Structure (DBM), pp. 277–286.

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.