Search results for "Type Theory"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
3	Zofia Kostrzycka, Marek Zaionc	Asymptotic Densities in Logic and Type Theory.	Studia Logica	2008	DBLP DOI BibTeX RDF	asymptotic density of tautologies, probabilistic methods in logic and type theory, propositional logic
3	Norihiro Ogata	Formal Ontology of 'Cultures' and 'Ethnic Groups' Based on Type Theory and Functional Programming.	IWIC	2007	DBLP DOI BibTeX RDF	Formal Cultural Ontology, qualia, ethnic group, Functional Programming, culture, Type Theory
3	Maria Emilia Maietti	Quotients over Minimal Type Theory.	CiE	2007	DBLP DOI BibTeX RDF	Dependent type theory, quotient completion, intuitionistic logic
3	Robin Adams, Zhaohui Luo	Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory.	TYPES	2006	DBLP DOI BibTeX RDF	logic-enriched type theory, predicativism, formalisation
3	Aleksandar Nanevski, Greg Morrisett, Lars Birkedal	Polymorphism and separation in hoare type theory.	ICFP	2006	DBLP DOI BibTeX RDF	type theory, hoare logic, separation logic
3	Anton Setzer	Partial Recursive Functions in Martin-Löf Type Theory.	CiE	2006	DBLP DOI BibTeX RDF	Martin-Löf type theory, Kleene index, Kleene brackets, partial recursive functions, inductive-recursive definitions, indexed induction-recursion, computability theory, recursion theory
3	Robert Harper, Frank Pfenning	On equivalence and canonical forms in the LF type theory.	ACM Trans. Comput. Log.	2005	DBLP DOI BibTeX RDF	type theory, Logical frameworks
3	Andreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell	Verifying haskell programs using constructive type theory.	Haskell	2005	DBLP DOI BibTeX RDF	GHC core, monadic translation, verification, haskell, type theory, partiality
3	Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning	A type theory for memory allocation and data layout.	POPL	2003	DBLP DOI BibTeX RDF	ordered logic, memory management, type theory, data representation
3	Peter Dybjer, Anton Setzer	Indexed Induction-Recursion.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF	Dependent type theory, Martin-Löf Type Theory, inductive-recursive definitions, inductive families, normalization proofs, generic programming, inductive definitions, initial algebras
3	Thorsten Altenkirch	Extensional Equality in Intensional Type Theory.	LICS	1999	DBLP DOI BibTeX RDF	Type Theory, categorical models
3	Daniel Fridlender	An Interpretation of the Fan Theorem in Type Theory.	TYPES	1998	DBLP DOI BibTeX RDF	fan theorem, inductive bar, type theory
3	Ivo G. Rosenberg	An Algebraic Approach to Hyperalgebras. (PDF / PS)	ISMVL	1996	DBLP DOI BibTeX RDF	hyperalgebras, hypergroups theory, universal-algebra type theory, nonvoid subsets, hyperclones, inclusion-isotone clones, subuniverses, algebra, type theory, Boolean algebra, Boolean algebra, congruences, algebraic approach
3	Ming-Yuan Zhu, Xiao-Bai Mo	Mechanical synthesis of a unification algorithm in PowerEpsilon. (PDF / PS)	COMPSAC	1995	DBLP DOI BibTeX RDF	PowerEpsilon, constructive type theory, proof development system, formal program development system, formal specification, specification, programming, theorem proving, programming theory, type theory, unification algorithm, mechanical synthesis
3	Leen Helmink	Resolution and Type Theory.	ESOP	1990	DBLP DOI BibTeX RDF	Calculus of Constructions, Type Theory, Natural Deduction, Typed Lambda Calculus
3	F. Keith Hanna, Neil Daeche, Mark Longley	Veritas+: A Specification Language Based on Type Theory.	Hardware Specification, Verification and Synthesis	1989	DBLP DOI BibTeX RDF	Formal verification, Specification languages, Type theory
2	Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine	Structuring the verification of heap-manipulating programs.	POPL	2010	DBLP DOI BibTeX RDF	type theory, monads, hoare logic, separation logic
2		Type Theory.	Encyclopedia of Database Systems	2009	DBLP DOI BibTeX RDF
2	Christoph Benzmüller	Automating Access Control Logics in Simple Type Theory with LEO-II.	SEC	2009	DBLP DOI BibTeX RDF
2	Peter LeFanu Lumsdaine	Weak omega-Categories from Intensional Type Theory.	TLCA	2009	DBLP DOI BibTeX RDF
2	Steven Awodey, Florian Rabe	Kripke Semantics for Martin-Löf's Extensional Type Theory.	TLCA	2009	DBLP DOI BibTeX RDF
2	Chad E. Brown, Gert Smolka	Terminating Tableaux for the Basic Fragment of Simple Type Theory.	TABLEAUX	2009	DBLP DOI BibTeX RDF
2	Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez	Embedding a logical theory of constructions in Agda.	PLPV	2009	DBLP DOI BibTeX RDF	general recursion, logical theory of constructions, type theory
2	Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller, Timothy W. Simpson	Verified programming in Guru.	PLPV	2009	DBLP DOI BibTeX RDF	dependently typed programming, language-based verification, operational type theory
2	Aleksandar Nanevski, Paul Govereau, Greg Morrisett	Towards type-theoretic semantics for transactional concurrency.	TLDI	2009	DBLP DOI BibTeX RDF	type theory, monads, hoare logic, separation logic
2	Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka	Contextual modal type theory.	ACM Trans. Comput. Log.	2008	DBLP DOI BibTeX RDF	intuitionistic modal logic, Type theory, logical frameworks
2	Herman Geuvers	Introduction to Type Theory.	LerNet ALFA Summer School	2008	DBLP DOI BibTeX RDF
2	Yuyu Yin, Jianwei Yin, Ying Li, ShuiGuang Deng	Verifying Consistency of Web Services Behavior Using Type Theory.	APSCC	2008	DBLP DOI BibTeX RDF
2	Andreas Abel, Thierry Coquand, Peter Dybjer	On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory.	FLOPS	2008	DBLP DOI BibTeX RDF
2	Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett	A Realizability Model for Impredicative Hoare Type Theory.	ESOP	2008	DBLP DOI BibTeX RDF
2	Ralph Matthes	Recursion on Nested Datatypes in Dependent Type Theory.	CiE	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	Yves Bertot, Ekaterina Komendantskaya	Using Structural Recursion for Corecursion.	TYPES	2008	DBLP DOI BibTeX RDF	Constructive Type Theory, Structural Recursion, Coinductive types, Guarded Corecursion, Coq
2	Alberto Ciaffaglione, Luigi Liquori, Marino Miculan	Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts.	J. Autom. Reasoning	2007	DBLP DOI BibTeX RDF	Functional and imperative object-calculi, Logical foundations of programming, Coinductive type theories, Logical frameworks, Interactive theorem proving
2	Milad Niqui	Productivity of Edalat-Potts Exact Arithmetic in Constructive Type Theory.	Theory Comput. Syst.	2007	DBLP DOI BibTeX RDF
2	Thierry Coquand, Arnaud Spiwack	Towards Constructive Homological Algebra in Type Theory.	Calculemus/MKM	2007	DBLP DOI BibTeX RDF
2	Qiao Haiyan	Testing and Proving Distributed Algorithms in Constructive Type Theory.	TAP	2007	DBLP DOI BibTeX RDF
2	Agnieszka Kozubek, Pawel Urzyczyn	In the Search of a Naive Type Theory.	TYPES	2007	DBLP DOI BibTeX RDF
2	Claudio Sacerdoti Coen, Enrico Tassi	Working with Mathematical Structures in Type Theory.	TYPES	2007	DBLP DOI BibTeX RDF
2	François Garillot, Benjamin Werner	Simple Types in Type Theory: Deep and Shallow Encodings.	TPHOLs	2007	DBLP DOI BibTeX RDF
2	Andreas Abel, Thierry Coquand, Peter Dybjer	Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements.	LICS	2007	DBLP DOI BibTeX RDF
2	Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, Lars Birkedal	Abstract Predicates and Mutable ADTs in Hoare Type Theory.	ESOP	2007	DBLP DOI BibTeX RDF
2	Thorsten Altenkirch, Conor McBride, Wouter Swierstra	Observational equality, now!	PLPV	2007	DBLP DOI BibTeX RDF	type theory, equality
2	Adam Megacz	A coinductive monad for prop-bounded recursion.	PLPV	2007	DBLP DOI BibTeX RDF	coinductive types, type theory
2	Vilém Novák	EQ-Algebras in Progress.	IFSA	2007	DBLP DOI BibTeX RDF	fuzzy type theory, higher-order fuzzy logic, fuzzy logic, Residuated lattice, fuzzy equality
2	Francesco Ciraulo, Giovanni Sambin	Finiteness in a Minimalist Foundation.	TYPES	2007	DBLP DOI BibTeX RDF	minimalist foundation, finite subsets, type theory, constructive mathematics, finite sets
2	Chad E. Brown	Combining Type Theory and Untyped Set Theory.	IJCAR	2006	DBLP DOI BibTeX RDF
2	Zhiwei Chen, Jian Wu, ShuiGuang Deng, Ying Li, Zhaohui Wu	Describing and Verifying Web Service Using Type Theory.	CSCWD	2006	DBLP DOI BibTeX RDF
2	Danko Ilik	Zermelo's Well-Ordering Theorem in Type Theory.	TYPES	2006	DBLP DOI BibTeX RDF
2	Björn Bringert, Aarne Ranta	A pattern for almost compositional functions.	ICFP	2006	DBLP DOI BibTeX RDF	dependent type theory, java, haskell, abstract syntax, traversal, visitor pattern
2	Iman Poernomo	The meta-object facility typed.	SAC	2006	DBLP DOI BibTeX RDF	constructive type theory, model driven architecture
2	Chad E. Brown	Reasoning in Extensional Type Theory with Equality.	CADE	2005	DBLP DOI BibTeX RDF
2	Healfdene Goguen	A syntactic approach to eta equality in type theory.	POPL	2005	DBLP DOI BibTeX RDF	beta-eta equality, decidability, type checking, logical frameworks
2	Frank Pfenning	Towards a type theory of contexts.	MERLIN	2005	DBLP DOI BibTeX RDF
2	Federico De Marchi	On the Semantics of Coinductive Types in Martin-Löf Type Theory.	CALCO	2005	DBLP DOI BibTeX RDF
2	Milad Niqui	Formalising Exact Arithmetic in Type Theory.	CiE	2005	DBLP DOI BibTeX RDF
2	Aleksey Nogin, Alexei Kopylov, Xin Yu, Jason Hickey	A computational approach to reflective meta-reasoning about languages with bindings.	MERLIN	2005	DBLP DOI BibTeX RDF	MetaPRL, Nuprl, languages with bindings, programming language, reflection, experimentation, type theory, higher-order abstract syntax
2	Jian-Min Pang, Paul Callaghan, Zhaohui Luo	LFTOP: An LF-Based Approach to Domain-Specific Reasoning.	J. Comput. Sci. Technol.	2005	DBLP DOI BibTeX RDF	type theory, logical framework, proof assistant, domain-specific, formal reasoning
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	Ana Bove, Thierry Coquand	Formalising Bitonic Sort in Type Theory.	TYPES	2004	DBLP DOI BibTeX RDF
2	Kwanghoon Choi, Atsushi Ohori	A Type Theory for Krivine-Style Evaluation and Compilation.	APLAS	2004	DBLP DOI BibTeX RDF
2	Ulrich Schöpp, Ian Stark	A Dependent Type Theory with Names and Binding.	CSL	2004	DBLP DOI BibTeX RDF
2	Marcelo P. Fiore	Isomorphisms of generic recursive polynomial types.	POPL	2004	DBLP DOI BibTeX RDF	Gröbner bases, type isomorphism, data structure, type theory, recursive types, word problem, semigroups, rigs
2	Robbert-Jan Beun, Rogier M. van Eijk, Hub Prüst	Ontological Feedback in Multiagent Systems.	AAMAS	2004	DBLP DOI BibTeX RDF	ontological feedback, ontological discrepancies, type theory, presuppositions
2	Marius C. Bujorianu	Integration of Specification Languages Using Viewpoints.	IFM	2004	DBLP DOI BibTeX RDF	Language integration, process algebra, Z, type theory, viewpoints, category theory
2	Fairouz Kamareddine, Rob Nederpelt	A Refinement of de Bruijn's Formal Language of Mathematics.	Journal of Logic, Language and Information	2004	DBLP DOI BibTeX RDF	mathematical vernacular, weak type theory, formal language, mathematics
2	Aarne Ranta, Robin Cooper	Dialogue Systems as Proof Editors.	Journal of Logic, Language and Information	2004	DBLP DOI BibTeX RDF	proof editing, type theory, dialogue
2	Michael Rathjen	Realizing Mahlo set theory in type theory.	Arch. Math. Log.	2003	DBLP DOI BibTeX RDF
2	Toshiyuki Maeda, Akinori Yonezawa	Kernel Mode Linux: Toward an Operating System Protected by a Type Theory.	ASIAN	2003	DBLP DOI BibTeX RDF
2	Vilém Novák	Towards Fuzzy Type Theory. (PDF / PS)	ISMVL	2003	DBLP DOI BibTeX RDF
2	Carlos Gonzalia	Towards a Formalisation of Relational Database Theory in Constructive Type Theory.	RelMiCS	2003	DBLP DOI BibTeX RDF
2	Peter Dybjer, Qiao Haiyan, Makoto Takeyama	Combining Testing and Proving in Dependent Type Theory.	TPHOLs	2003	DBLP DOI BibTeX RDF
2	Alexei Kopylov	Dependent Intersection: A New Way of Defining Records in Type Theory.	LICS	2003	DBLP DOI BibTeX RDF
2	Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning	A modal foundation for meta-variables.	MERLIN	2003	DBLP DOI BibTeX RDF	modal type theory, pattern unification, logical frameworks
2	Derek Dreyer, Karl Crary, Robert Harper	A type system for higher-order modules.	POPL	2003	DBLP DOI BibTeX RDF	modularity, generativity, abstract data types, type theory, computational effects, singleton types, functors
2	Peter Dybjer, Qiao Haiyan, Makoto Takeyama	Verifying Haskell Programs by Combining Testing and Proving.	QSIC	2003	DBLP DOI BibTeX RDF	BDDs and Haskell, program verification, random testing, type theory, proof-assistants
2	Horatiu Cirstea, Luigi Liquori, Benjamin Wack	Rewriting Calculus with Fixpoints: Untyped and First-Order Systems.	TYPES	2003	DBLP DOI BibTeX RDF	Rewriting-calculus, Object-calculus, Pattern Mat-ching, Lambda-calculus, Type Theory, Fixpoints
2	Jesper Carlström	Subsets, Quotients and Partial Functions in Martin-Löf's Type Theory.	TYPES	2002	DBLP DOI BibTeX RDF
2	Ana Bove	General Recursion in Type Theory.	TYPES	2002	DBLP DOI BibTeX RDF
2	Karl Crary, Joseph Vanderwaart	An expressive, scalable type theory for certified code.	ICFP	2002	DBLP DOI BibTeX RDF
2	Herman Geuvers, Gueorgui I. Jojgov	Open Proofs and Open Terms: A Basis for Interactive Logic.	CSL	2002	DBLP DOI BibTeX RDF	open terms, meta-variables, formulas-as-types, type theory, interactive theorem proving
2	Jean-Paul Bodeveix, Mamoun Filali	Type Synthesis in B and the Translation of B to PVS.	ZB	2002	DBLP DOI BibTeX RDF	semantics, type theory, PVS, logical frameworks, B
2	Michael Rathjen	The strength of Martin-Löf type theory with a superuniverse. Part II.	Arch. Math. Log.	2001	DBLP DOI BibTeX RDF
2	Herman Geuvers	Induction Is Not Derivable in Second Order Dependent Type Theory.	TLCA	2001	DBLP DOI BibTeX RDF
2	Ana Bove, Venanzio Capretta	Nested General Recursion and Partiality in Type Theory.	TPHOLs	2001	DBLP DOI BibTeX RDF
2	James L. Caldwell	Extracting General Recursive Program Schemes in Nuprl's Type Theory.	LOPSTR	2001	DBLP DOI BibTeX RDF
2	Alexei Kopylov, Aleksey Nogin	Markov's Principle for Propositional Type Theory.	CSL	2001	DBLP DOI BibTeX RDF
2	Michael Rathjen	The strength of Martin-Löf type theory with a superuniverse. Part I.	Arch. Math. Log.	2000	DBLP DOI BibTeX RDF
2	Anton Setzer	Extending Martin-Löf Type Theory by one Mahlo-universe.	Arch. Math. Log.	2000	DBLP DOI BibTeX RDF
2	Marc Bezem, Dimitri Hendriks, Hans de Nivelle	Automated Proof Construction in Type Theory Using Resolution.	CADE	2000	DBLP DOI BibTeX RDF
2	Peter B. Andrews, Matthew Bishop, Chad E. Brown	System Description: TPS: A Theorem Proving System for Type Theory.	CADE	2000	DBLP DOI BibTeX RDF
2	Kristofer Johannisson	Formalizing the Halting Problem in a Constructive Type Theory.	TYPES	2000	DBLP DOI BibTeX RDF
2	Nicolas Magaud, Yves Bertot	Changing Data Structures in Type Theory: A Study of Natural Numbers.	TYPES	2000	DBLP DOI BibTeX RDF
2	Matt Fairtlough, Michael Mendler	On the Logical Content of Computational Type Theory: A Solution to Curry's Problem.	TYPES	2000	DBLP DOI BibTeX RDF
2	Olivier Pons	Generalization in Type Theory Based Proof Assistants.	TYPES	2000	DBLP DOI BibTeX RDF
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	Maria Emilia Maietti, Valeria de Paiva, Eike Ritter	Categorical Models for Intuitionistic and Linear Type Theory.	FoSSaCS	2000	DBLP DOI BibTeX RDF
2	David Aspinall	Subtyping with Power Types.	CSL	2000	DBLP DOI BibTeX RDF	subtyping, type theory, dependent types
2	Andrej Bauer, Lars Birkedal	Continuous Functionals of Dependent Types and Equilogical Spaces.	CSL	2000	DBLP DOI BibTeX RDF	dependent type theory, equilogical spaces, domain theory, continuous functionals
2	Geir Waagbø	Denotational semantics for intuitionistic type theory using a hierarchy of domains with totality.	Arch. Math. Log.	1999	DBLP DOI BibTeX RDF