Search results for "dependent types"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
3	Tachio Terauchi	Dependent types from counterexamples.	POPL	2010	DBLP DOI BibTeX RDF	interpolation, type inference, dependent types, counterexamples, intersection types
3	Daniel R. Licata, Robert Harper	Positively dependent types.	PLPV	2009	DBLP DOI BibTeX RDF	agda, dependent types, polarity
3	Cherif Salama, Gregory Malecha, Walid Taha, Jim Grundy, John O'Leary	Static consistency checking for verilog wire interconnects: using dependent types to check the sanity of verilog descriptions.	PEPM	2009	DBLP DOI BibTeX RDF	static array bounds checking, verilog elaboration, verilog wire width consistency, dependent types, dead code elimination
3	Neil Sculthorpe, Henrik Nilsson	Safe functional reactive programming through dependent types.	ICFP	2009	DBLP DOI BibTeX RDF	DSELS, FRP, synchronous data-flow, functional programming, domain-specific languages, dependent types, reactive programming
3	Iliano Cervesato, Mark-Oliver Stehr	Representing the MSR cryptoprotocol specification language in an extension of rewriting logic with dependent types.	Higher-Order and Symbolic Computation	2007	DBLP DOI BibTeX RDF	Multiset rewriting, Specification, Security protocol, Dependent types
3	Conor McBride	What's the deal with dependent types?	TLDI	2007	DBLP DOI BibTeX RDF	epigram, pattern matching, dependent types
3	Hongwei Xi	Imperative Programming with Dependent Types.	LICS	2000	DBLP DOI BibTeX RDF	dependent types, programming language design, array bounds checking
3	Ulrich Berger	Density Theorems for the Domains-with-Totality Semantics of Dependent Types.	Applied Categorical Structures	1999	DBLP DOI BibTeX RDF	totality, dependent types, universes, domains, continuous functionals
3	Lennart Augustsson	Cayenne - a Language with Dependent Types.	ICFP	1998	DBLP DOI BibTeX RDF	type systems, language design, dependent types, module systems
3	F. Keith Hanna, Neil Daeche, Mark Longley	Specification and Verification Using Dependent Types.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	VERITAS/sup +/, iterative structures, functional metalanguage, computational implementation, modeling, modelling, formal specification, theorem proving, theorem proving, iterative methods, dependent types, numerals, specification logic
2	Limin Jia, Jianzhou Zhao, Vilhelm Sjöberg, Stephanie Weirich	Dependent types and program equivalence.	POPL	2010	DBLP DOI BibTeX RDF	dependent types, program equivalence
2	Adam Chlipala	Ur: statically-typed metaprogramming with type-level record computation.	PLDI	2010	DBLP DOI BibTeX RDF	dependent types, metaprogramming
2	Stefan Monnier, David Haguenauer	Singleton types here, singleton types there, singleton types everywhere.	PLPV	2010	DBLP DOI BibTeX RDF	dependent types, certified compilation, singleton types
2	Stephanie Weirich, Chris Casinghino	Arity-generic datatype-generic programming.	PLPV	2010	DBLP DOI BibTeX RDF	agda, arity-generic programming, generic haskell, dependent types
2	Wojciech Moczydlowski	Unifying Sets and Programs via Dependent Types.	LFCS	2009	DBLP DOI BibTeX RDF
2	Hiroshi Unno, Naoki Kobayashi	Dependent type inference with interpolants.	PPDP	2009	DBLP DOI BibTeX RDF	type inference, dependent types
2	Ulf Norell	Dependently typed programming in Agda.	TLDI	2009	DBLP DOI BibTeX RDF	programming, dependent types
2	Ana Bove, Peter Dybjer	Dependent Types at Work.	LerNet ALFA Summer School	2008	DBLP DOI BibTeX RDF
2	Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal	Ynot: dependent types for imperative programs.	ICFP	2008	DBLP DOI BibTeX RDF	type theory, monads, Hoare logic, separation logic
2	Hiroshi Unno, Naoki Kobayashi	On-Demand Refinement of Dependent Types.	FLOPS	2008	DBLP DOI BibTeX RDF
2	Bruno Barras, Bruno Bernardo	The Implicit Calculus of Constructions as a Programming Language with Dependent Types.	FoSSaCS	2008	DBLP DOI BibTeX RDF
2	Adam Poswolsky, Carsten Schürmann	Practical Programming with Higher-Order Encodings and Dependent Types.	ESOP	2008	DBLP DOI BibTeX RDF
2	Nicolas Oury, Wouter Swierstra	The power of Pi.	ICFP	2008	DBLP DOI BibTeX RDF	domain-specific embedded languages, dependent types
2	Nathaniel Nystrom, Vijay A. Saraswat, Jens Palsberg, Christian Grothoff	Constrained types for object-oriented languages.	OOPSLA	2008	DBLP DOI BibTeX RDF	constraints, dependent types, object-oriented programming languages
2	Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala	Liquid types.	PLDI	2008	DBLP DOI BibTeX RDF	hindley-milner, type inference, dependent types, predicate abstraction
2	Nicolas Oury	Pattern matching coverage checking with dependent types using set approximations.	PLPV	2007	DBLP DOI BibTeX RDF	coverage checking, set approximation, pattern matching
2	Robert Atkey	CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types.	TYPES	2007	DBLP DOI BibTeX RDF
2	Dirk Kleeblatt	Checking Dependent Types Using Compiled Code.	IFL	2007	DBLP DOI BibTeX RDF
2	Jeremy Condit, Matthew Harren, Zachary R. Anderson, David Gay, George C. Necula	Dependent Types for Low-Level Programming.	ESOP	2007	DBLP DOI BibTeX RDF
2	Adam Chlipala	A certified type-preserving compiler from lambda calculus to assembly language.	PLDI	2007	DBLP DOI BibTeX RDF	denotational semantics, dependent types, compiler verification, interactive proof assistants
2	Kathleen Fisher	Typing ad hoc data.	TLDI	2007	DBLP DOI BibTeX RDF	ad hoc data, domain-specific languages, dependent types, data description languages
2	Florian Rabe	First-Order Logic with Dependent Types.	IJCAR	2006	DBLP DOI BibTeX RDF
2	George C. Necula	Using Dependent Types to Port Type Systems to Low-Level Languages.	CC	2006	DBLP DOI BibTeX RDF
2	Edwin Brady, Kevin Hammond	A verified staged interpreter is a verified compiler.	GPCE	2006	DBLP DOI BibTeX RDF	domain specific language implementation, resource aware programming, functional programming, partial evaluation, dependent types, multi-stage programming
2	Adam Chlipala	Modular development of certified program verifiers with a proof assistant.	ICFP	2006	DBLP DOI BibTeX RDF	programming with dependent types, proof-carrying code, interactive proof assistants
2	DeLesley Hutchins	Eliminating distinctions of class: using prototypes to model virtual classes.	OOPSLA	2006	DBLP DOI BibTeX RDF	virtual types, prototypes, abstract interpretation, partial evaluation, features, dependent types, mixins, virtual classes, singleton types
2	Kathleen Fisher, Yitzhak Mandelbaum, David Walker	The next 700 data description languages.	POPL	2006	DBLP DOI BibTeX RDF	domain-specific languages, dependent types, data description language
2	Raghavan Komondoor, Ganesan Ramalingam, Satish Chandra, John Field	Dependent Types for Program Understanding.	TACAS	2005	DBLP DOI BibTeX RDF
2	Matthew Harren, George C. Necula	Using Dependent Types to Certify the Safety of Assembly Code.	SAS	2005	DBLP DOI BibTeX RDF
2	Kevin Donnelly, Hongwei Xi	Combining higher-order abstract syntax with first-order abstract syntax in ATS.	MERLIN	2005	DBLP DOI BibTeX RDF	ATS/LF, theorem proving, dependent types, higher-order abstract syntax, ATS
2	Edwin M. Westbrook, Aaron Stump, Ian Wehrman	A language-based approach to functionally correct imperative programming.	ICFP	2005	DBLP DOI BibTeX RDF	RSP, RSP1, program verification, dependent types
2	Chiyan Chen, Dengping Zhu, Hongwei Xi	Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell.	PADL	2004	DBLP DOI BibTeX RDF
2	Nobuko Yoshida	Channel dependent types for higher-order mobile processes.	POPL	2004	DBLP DOI BibTeX RDF	the higher-order ?-calculus, access control, types, secrecy, mobile processes
2	Joshua Dunfield, Frank Pfenning	Tridirectional typechecking.	POPL	2004	DBLP DOI BibTeX RDF	type refinements, dependent types, intersection types, union types
2	Solange Coupet-Grimal, Line Jakubiec	Certifying circuits in Type Theory.	Formal Asp. Comput.	2004	DBLP DOI BibTeX RDF	Co-induction, Formal methods, Type theory, Dependent types, Extraction, Hardware verification
2	Hongwei Xi	Facilitating Program Verification with Dependent Types.	SEFM	2003	DBLP DOI BibTeX RDF
2	Robert Pollack	Dependently Typed Records in Type Theory.	Formal Asp. Comput.	2002	DBLP DOI BibTeX RDF	Inductive-recursive, Manifest types, Signature, Module, Sharing, Dependent types, Pebble
2	David Aspinall	Subtyping with Power Types.	CSL	2000	DBLP DOI BibTeX RDF	subtyping, type theory, dependent types
2	Peter Hancock, Anton Setzer	Interactive Programs in Dependent Type Theory.	CSL	2000	DBLP DOI BibTeX RDF	monadic I/O, repetition constructs, interaction, refinement, Functional programming, dependent types, reactive programming
2	Hongwei Xi	Dead Code Elimination through Dependent Types.	PADL	1999	DBLP DOI BibTeX RDF
2	Hongwei Xi, Frank Pfenning	Eliminating Array Bound Checking Through Dependent Types.	PLDI	1998	DBLP DOI BibTeX RDF	Standard ML
2	Florian Kammüller	Modular Structures as Dependent Types in Isabelle.	TYPES	1998	DBLP DOI BibTeX RDF
2	Neal Nelson	Primitive Recursive Functionals with Dependent Types.	MFPS	1991	DBLP DOI BibTeX RDF
2	Bernd Krieg-Brückner, Donald Sannella	Structuring Specifications in-the-Large and in-the-Small: Higher-Order Functions, Dependent Types and Inheritance in SPECTRAL.	TAPSOFT, Vol.2	1991	DBLP DOI BibTeX RDF
2	Mark A. Sheldon, David K. Gifford	Static Dependent Types for First Class Modules.	LISP and Functional Programming	1990	DBLP DOI BibTeX RDF	LISP
1	Wojciech Moczydlowski	Unifying sets and programs via dependent types.	Ann. Pure Appl. Logic	2012	DBLP DOI BibTeX RDF
1	Ravi Chugh, Ranjit Jhala	Dependent Types for JavaScript	CoRR	2011	DBLP BibTeX RDF
1	Ugo Dal Lago, Marco Gaboardi	Linear Dependent Types and Relative Completeness	CoRR	2011	DBLP BibTeX RDF
1	Aleksandar Nanevski, Anindya Banerjee, Deepak Garg	Verification of Information Flow and Access Control Policies with Dependent Types.	IEEE Symposium on Security and Privacy	2011	DBLP DOI BibTeX RDF	Access Control, Information Flow, Type Theory
1	Andreas Abel, Brigitte Pientka	Higher-Order Dynamic Pattern Unification for Dependent Types and Records.	TLCA	2011	DBLP DOI BibTeX RDF
1	Kasper Svendsen, Lars Birkedal, Aleksandar Nanevski	Partiality, State and Dependent Types.	TLCA	2011	DBLP DOI BibTeX RDF
1	Edwin Brady	IDRIS ---: systems programming meets full dependent types.	PLPV	2011	DBLP DOI BibTeX RDF
1	Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang	Secure distributed programming with value-dependent types.	ICFP	2011	DBLP DOI BibTeX RDF
1	Ugo Dal Lago, Marco Gaboardi	Linear Dependent Types and Relative Completeness.	LICS	2011	DBLP DOI BibTeX RDF
1	Ralf Hinze, Daniel W. H. James	Proving the unique fixed-point principle correct: an adventure with category theory.	ICFP	2011	DBLP DOI BibTeX RDF
1	Richard Dapoigny, Patrick Barlatier	Modeling Contexts with Dependent Types.	Fundam. Inform.	2010	DBLP DOI BibTeX RDF
1	Edwin Brady, Kevin Hammond	Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols.	Fundam. Inform.	2010	DBLP DOI BibTeX RDF
1	Andreas Abel	MiniAgda: Integrating Sized and Dependent Types	PAR	2010	DBLP DOI BibTeX RDF
1	Wouter Swierstra	More dependent types for distributed arrays.	Higher-Order and Symbolic Computation	2010	DBLP DOI BibTeX RDF
1	Richard Dapoigny, Patrick Barlatier	Towards Ontological Correctness of Part-whole Relations with Dependent Types.	FOIS	2010	DBLP DOI BibTeX RDF
1	Jean-Philippe Bernardy, Patrik Jansson, Ross Paterson	Parametricity and dependent types.	ICFP	2010	DBLP DOI BibTeX RDF
1	Brigitte Pientka	Beluga: Programming with Dependent Types, Contextual Data, and Contexts.	FLOPS	2010	DBLP DOI BibTeX RDF
1	Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, Nicolas Oury	PiSigma: Dependent Types without the Sugar.	FLOPS	2010	DBLP DOI BibTeX RDF
1	Juan Chen, Ravi Chugh, Nikhil Swamy	Type-preserving compilation of end-to-end verification of security enforcement.	PLDI	2010	DBLP DOI BibTeX RDF	bytecode languages, compilers, authorization, functional programming, information flow, dependent types, security type systems, mobile code security
1	Matthew Danish, Hongwei Xi	Operating system development with ATS: work in progress.	PLPV	2010	DBLP DOI BibTeX RDF	linear types, operating systems, dependent types
1	DeLesley S. Hutchins	Pure subtype systems.	POPL	2010	DBLP DOI BibTeX RDF	abstract reduction systems, transitivity elimination, subtyping, dependent types, singleton types
1	J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky	Toward a verified relational database management system.	POPL	2010	DBLP DOI BibTeX RDF	relational model, dependent types, separation logic, b+ tree
1	Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala	Low-level liquid types.	POPL	2010	DBLP DOI BibTeX RDF	liquid types, c, type inference, dependent types
1	Shin-Cheng Mu, Hsiang-Shang Ko, Patrik Jansson	Algebra of programming in Agda: Dependent types for relational program derivation.	J. Funct. Program.	2009	DBLP DOI BibTeX RDF
1	Richard Dapoigny, Patrick Barlatier	Reasoning about Relations with Dependent Types: Application to Context-Aware Applications.	ISMIS	2009	DBLP DOI BibTeX RDF
1	Richard Dapoigny, Patrick Barlatier	Towards an Ontological Modeling with Dependent Types: Application to Part-Whole Relations.	ER	2009	DBLP DOI BibTeX RDF
1	Ana Bove, Peter Dybjer, Ulf Norell	A Brief Overview of Agda - A Functional Language with Dependent Types.	TPHOLs	2009	DBLP DOI BibTeX RDF
1	Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky	Effective interactive proofs for higher-order imperative programs.	ICFP	2009	DBLP DOI BibTeX RDF	functional programming, dependent types, separation logic, interactive proof assistants
1	Daniel R. Licata, Robert Harper	A universe of binding and computation.	ICFP	2009	DBLP DOI BibTeX RDF	dependent types, variable binding
1	Ming Kawaguchi, Patrick Maxim Rondon, Ranjit Jhala	Type-based data structure verification.	PLDI	2009	DBLP DOI BibTeX RDF	hindley-milner, type inference, dependent types, predicate abstraction
1	Kenneth L. Knowles, Cormac Flanagan	Compositional reasoning and decidable checking for dependent contract types.	PLPV	2009	DBLP DOI BibTeX RDF	refinement types, abstraction, dependent types, compositional reasoning
1	Eva K. Lee	Machine Learning Framework for Classification in Medicine and Biology.	CPAIOR	2009	DBLP DOI BibTeX RDF
1	William Lovas, Frank Pfenning	Refinement Types as Proof Irrelevance.	TLCA	2009	DBLP DOI BibTeX RDF
1	Patrick Barlatier, Richard Dapoigny	A Theorem Prover with Dependent Types for Reasoning about Actions.	STAIRS	2008	DBLP DOI BibTeX RDF
1	Richard Dapoigny, Patrick Barlatier	Causal Reasoning with Contexts Using Dependent Types.	FLAIRS Conference	2008	DBLP BibTeX RDF
1	Shin-Cheng Mu, Hsiang-Shang Ko, Patrik Jansson	Algebra of Programming Using Dependent Types.	MPC	2008	DBLP DOI BibTeX RDF
1	Kai Trojahner, Clemens Grelck	Descriptor-Free Representation of Arrays with Dependent Types.	IFL	2008	DBLP DOI BibTeX RDF
1	Adam Chlipala	Parametric higher-order abstract syntax for mechanized semantics.	ICFP	2008	DBLP DOI BibTeX RDF	type-theoretic semantics, dependent types, compiler verification, interactive proof assistants
1	Corneliu Popeea, Dana N. Xu, Wei-Ngan Chin	A practical and precise inference and specializer for array bound checks elimination.	PEPM	2008	DBLP DOI BibTeX RDF	size properties, dependent types, safety verification
1	Nils Anders Danielsson	Lightweight semiformal time complexity analysis for purely functional data structures.	POPL	2008	DBLP DOI BibTeX RDF	amortised time complexity, purely functional data structures, dependent types, lazy evaluation
1	Brigitte Pientka, Joshua Dunfield	Programming with proofs and explicit contexts.	PPDP	2008	DBLP DOI BibTeX RDF	type theory, dependent types, logical frameworks
1	Nikhil Swamy, Michael Hicks	Verified enforcement of stateful information release policies.	SIGPLAN Notices	2008	DBLP DOI BibTeX RDF	affine types, certified evaluation, state modifying policies, dependent types, declassification, singleton types
1	Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, Steve Zdancewic	AURA: a programming language for authorization and audit.	ICFP	2008	DBLP DOI BibTeX RDF	access control, type systems, audit, authorization logic
1	Yves Bertot	A Short Presentation of Coq.	TPHOLs	2008	DBLP DOI BibTeX RDF
1	Kristina Sojakova, Florian Rabe	Translating a Dependently-Typed Logic to First-Order Logic.	WADT	2008	DBLP DOI BibTeX RDF