Search results for "Types"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
33	Daniel Smith 0003, Robert Cartwright	Java type inference is broken: can we fix it?	OOPSLA	2008	DBLP DOI BibTeX RDF	bounded quantification, polymorphic methods, type argument inference, generics, type inference, subtyping, intersection types, union types, wildcards, parameterized types
33	Kathleen Fisher	Typing ad hoc data.	TLDI	2007	DBLP DOI BibTeX RDF	ad hoc data, domain-specific languages, dependent types, data description languages
32	Ole Agesen	The Cartesian Product Algorithm: Simple and Precise Type Inference Of Parametric Polymorphism.	ECOOP	1995	DBLP DOI BibTeX RDF	concrete types, inheritance, polymorphism, type inference, Self, abstract types
32	Andreas Rossberg	Generativity and dynamic opacity for abstract types.	PPDP	2003	DBLP DOI BibTeX RDF	generativity, encapsulation, opacity, dynamic typing, abstract types, existential types
32	Jean-Francois Girard, Rainer Koschke, Georg Schied	A Metric-based Approach to Detect Abstract Data Types and State Encapsulations.	ASE	1997	DBLP DOI BibTeX RDF	metric-based approach, state encapsulations, abstract objects, C systems, software engineers, abstract data types, abstract data types, source code
32	Norihisa Suzuki	Inferring Types in Smalltalk.	POPL	1981	DBLP DOI BibTeX RDF
32	Delia Kesner, Pierre-Marie Pédrot (eds.)	28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France	TYPES	2023	DBLP BibTeX RDF
32	Henning Basold, Jesper Cockx, Silvia Ghilezan (eds.)	27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference).	TYPES	2022	DBLP BibTeX RDF
32	Luca Padovani	On the Fair Termination of Client-Server Sessions.	TYPES	2022	DBLP DOI BibTeX RDF
32	Philipp Stassen, Daniel Gratzer, Lars Birkedal	{mitten}: A Flexible Multimodal Proof Assistant.	TYPES	2022	DBLP DOI BibTeX RDF
32	Catherine Dubois, Nicolas Magaud, Alain Giorgetti	Pragmatic Isomorphism Proofs Between Coq Representations: Application to Lambda-Term Families.	TYPES	2022	DBLP DOI BibTeX RDF
32	Andrea Colledan, Ugo Dal Lago	On Dynamic Lifting and Effect Typing in Circuit Description Languages.	TYPES	2022	DBLP DOI BibTeX RDF
32	Max Zeuner, Anders Mörtberg	A Univalent Formalization of Constructive Affine Schemes.	TYPES	2022	DBLP DOI BibTeX RDF
32	Marc Bezem, Thierry Coquand, Peter Dybjer, Martín Escardó	Type Theory with Explicit Universe Polymorphism.	TYPES	2022	DBLP DOI BibTeX RDF
32	Amélie Ledein, Valentin Blot, Catherine Dubois	A Semantics of	TYPES	2022	DBLP DOI BibTeX RDF
32	Herman Geuvers, Tonny Hurkens	Classical Natural Deduction from Truth Tables.	TYPES	2022	DBLP DOI BibTeX RDF
32	Dominic P. Mulligan	All Watched Over by Machines of Loving Grace.	TYPES	2022	DBLP DOI BibTeX RDF
32	Émilie Grienenberger	Expressing Ecumenical Systems in the λΠ-Calculus Modulo Theory.	TYPES	2022	DBLP DOI BibTeX RDF
32	Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, Tamás Végh	The Münchhausen Method in Type Theory.	TYPES	2022	DBLP DOI BibTeX RDF
32	Nathan Mull	An Irrelevancy-Eliminating Translation of Pure Type Systems.	TYPES	2022	DBLP DOI BibTeX RDF
32	Felix Bradley, Zhaohui Luo	A Metatheoretic Analysis of Subtype Universes.	TYPES	2022	DBLP DOI BibTeX RDF
32	Kobe Wullaert, Ralph Matthes, Benedikt Ahrens	Univalent Monoidal Categories.	TYPES	2022	DBLP DOI BibTeX RDF
32		Front Matter, Table of Contents, Preface, Conference Organization.	TYPES	2022	DBLP DOI BibTeX RDF
32	Ugo de'Liguoro, Stefano Berardi, Thorsten Altenkirch (eds.)	26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy.	TYPES	2021	DBLP BibTeX RDF
32	Giulio Fellin, Sara Negri, Eugenio Orlandelli	Constructive Cut Elimination in Geometric Logic.	TYPES	2021	DBLP DOI BibTeX RDF
32	Georgi Nakov, Fredrik Nordvall Forsberg	Quantitative Polynomial Functors.	TYPES	2021	DBLP DOI BibTeX RDF
32	Thibaut Benjamin	Formalisation of Dependent Type Theory: The Example of CaTT.	TYPES	2021	DBLP DOI BibTeX RDF
32		Front Matter, Table of Contents, Preface, Conference Organization.	TYPES	2021	DBLP DOI BibTeX RDF
32	Fahad F. Alhabardi, Arnold Beckmann, Bogdan Lazar, Anton Setzer	Verification of Bitcoin Script in Agda Using Weakest Preconditions for Access Control.	TYPES	2021	DBLP DOI BibTeX RDF
32	Asta Halkjær From	A Succinct Formalization of the Completeness of First-Order Logic.	TYPES	2021	DBLP DOI BibTeX RDF
32	Christa Jenkins, Andrew Marmaduke, Aaron Stump	Simulating Large Eliminations in Cedille.	TYPES	2021	DBLP DOI BibTeX RDF
32	István Donkó, Ambrus Kaposi	Internal Strict Propositions Using Point-Free Equations.	TYPES	2021	DBLP DOI BibTeX RDF
32	Rafaël Bocquet	Strictification of Weakly Stable Type-Theoretic Structures Using Generic Contexts.	TYPES	2021	DBLP DOI BibTeX RDF
32	William J. DeMeo, Jacques Carette	A Machine-Checked Proof of Birkhoff's Variety Theorem in Martin-Löf Type Theory.	TYPES	2021	DBLP DOI BibTeX RDF
32	Marc Bezem, Assia Mahboubi (eds.)	25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway.	TYPES	2020	DBLP BibTeX RDF
32	Andreas Abel 0001	On Model-Theoretic Strong Normalization for Truth-Table Natural Deduction.	TYPES	2020	DBLP DOI BibTeX RDF
32	Matteo Manighetti, Dale Miller 0001, Alberto Momigliano	Two Applications of Logic Programming to Coq.	TYPES	2020	DBLP DOI BibTeX RDF
32	Reynald Affeldt, David Nowak	Extending Equational Monadic Reasoning with Monad Transformers.	TYPES	2020	DBLP DOI BibTeX RDF
32		Front Matter, Table of Contents, Preface, Conference Organization.	TYPES	2020	DBLP DOI BibTeX RDF
32	Pawel Urzyczyn	Duality in Intuitionistic Propositional Logic.	TYPES	2020	DBLP DOI BibTeX RDF
32	Harry Maclean, Zhaohui Luo	Subtype Universes.	TYPES	2020	DBLP DOI BibTeX RDF
32	José Espírito Santo, Ralph Matthes, Luís Pinto 0001	Coinductive Proof Search for Polarized Logic with Applications to Full Intuitionistic Propositional Logic.	TYPES	2020	DBLP DOI BibTeX RDF
32	Jasper Hugunin	Why Not W?	TYPES	2020	DBLP DOI BibTeX RDF
32	Gabriel Hondet, Frédéric Blanqui	Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory.	TYPES	2020	DBLP DOI BibTeX RDF
32	Asta Halkjær From	Synthetic Completeness for a Terminating Seligman-Style Tableau System.	TYPES	2020	DBLP DOI BibTeX RDF
32	Guido De Luca, Carlos Luna 0001	Towards a Certified Reference Monitor of the Android 10 Permission System.	TYPES	2020	DBLP DOI BibTeX RDF
32	Peter Dybjer, José Espírito Santo, Luís Pinto 0001 (eds.)	24th International Conference on Types for Proofs and Programs, TYPES 2018, June 18-21, 2018, Braga, Portugal.	TYPES	2019	DBLP BibTeX RDF
32	Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, Stephanie Weirich	Eta-Equivalence in Core Dependent Haskell.	TYPES	2019	DBLP DOI BibTeX RDF
32	Nils Anders Danielsson	Higher Inductive Type Eliminators Without Paths.	TYPES	2019	DBLP DOI BibTeX RDF
32		Front Matter, Table of Contents, Preface, Conference Organization.	TYPES	2019	DBLP DOI BibTeX RDF
32	Stefano Piceghello	Coherence for Monoidal Groupoids in HoTT.	TYPES	2019	DBLP DOI BibTeX RDF
32	Gun Pinyo, Nicolai Kraus	From Cubes to Twisted Cubes via Graph Morphisms in Type Theory.	TYPES	2019	DBLP DOI BibTeX RDF
32	Stefan Monnier, Nathaniel Bos	Is Impredicativity Implicitly Implicit?	TYPES	2019	DBLP DOI BibTeX RDF
32	Michael Kohlhase, Florian Rabe 0001, Makarius Wenzel	Making Isabelle Content Accessible in Knowledge Representation Formats.	TYPES	2019	DBLP DOI BibTeX RDF
32	Sandra Alves, Delia Kesner, Daniel Ventura	A Quantitative Understanding of Pattern Matching.	TYPES	2019	DBLP DOI BibTeX RDF
32	Ambrus Kaposi, András Kovács, Ambroise Lafont	For Finitary Induction-Induction, Induction Is Enough.	TYPES	2019	DBLP DOI BibTeX RDF
32	Jesper Cockx	Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules.	TYPES	2019	DBLP DOI BibTeX RDF
32	Thorsten Altenkirch, Colin Geniet	Big Step Normalisation for Type Theory.	TYPES	2019	DBLP DOI BibTeX RDF
32	Andreas Abel 0001, Fredrik Nordvall Forsberg, Ambrus Kaposi (eds.)	23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary	TYPES	2018	DBLP BibTeX RDF
32	Tarmo Uustalu (eds.)	21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia	TYPES	2018	DBLP BibTeX RDF
32	Silvia Ghilezan, Herman Geuvers, Jelena Ivetic (eds.)	22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia	TYPES	2018	DBLP BibTeX RDF
32	Taichi Uemura	Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing.	TYPES	2018	DBLP DOI BibTeX RDF
32	Anders Schlichtkrull	New Formalized Results on the Meta-Theory of a Paraconsistent Logic.	TYPES	2018	DBLP DOI BibTeX RDF
32	Tommaso Petrucciani, Giuseppe Castagna, Davide Ancona, Elena Zucca	Semantic Subtyping for Non-Strict Languages.	TYPES	2018	DBLP DOI BibTeX RDF
32		Front Matter, Table of Contents, Preface, Conference Organization.	TYPES	2018	DBLP DOI BibTeX RDF
32	Iosif Petrakis	Dependent Sums and Dependent Products in Bishop's Set Theory.	TYPES	2018	DBLP DOI BibTeX RDF
32	Andrej Dudenhefner, Jakob Rehof	A Simpler Undecidability Proof for System F Inhabitation.	TYPES	2018	DBLP DOI BibTeX RDF
32	Filippo Sestini	Normalization by Evaluation for Typed Weak lambda-Reduction.	TYPES	2018	DBLP DOI BibTeX RDF
32	Guillaume Allais	Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic.	TYPES	2017	DBLP DOI BibTeX RDF
32	Andrej Dudenhefner, Jakob Rehof	Lower End of the Linial-Post Spectrum.	TYPES	2017	DBLP DOI BibTeX RDF
32		Front Matter, Table of Contents, Preface, Conference Organization.	TYPES	2017	DBLP DOI BibTeX RDF
32	Ian Orton, Andrew M. Pitts	Decomposing the Univalence Axiom.	TYPES	2017	DBLP DOI BibTeX RDF
32	Julius Michaelis, Tobias Nipkow	Formalized Proof Systems for Propositional Logic.	TYPES	2017	DBLP DOI BibTeX RDF
32	Erik Palmgren	On Equality of Objects in Categories in Constructive Type Theory.	TYPES	2017	DBLP DOI BibTeX RDF
32	Rodolphe Lepigre	PML2: Integrated Program Verification in ML.	TYPES	2017	DBLP DOI BibTeX RDF
32	Herman Geuvers, Tonny Hurkens	Proof Terms for Generalized Natural Deduction.	TYPES	2017	DBLP DOI BibTeX RDF
32	Jacek Chrzaszcz, Aleksy Schubert, Jakub Zakrzewski 0001	Coq Support in HAHA.	TYPES	2016	DBLP DOI BibTeX RDF
32	Marc Bezem, Thierry Coquand, Keiko Nakata 0001, Erik Parmann	Realizability at Work: Separating Two Constructive Notions of Finiteness.	TYPES	2016	DBLP DOI BibTeX RDF
32	Georgiana E. Lungu, Zhaohui Luo	On Subtyping in Type Theories with Canonical Objects.	TYPES	2016	DBLP DOI BibTeX RDF
32	Federico Aschieri, Matteo Manighetti	On Natural Deduction for Herbrand Constructive Logics II: Curry-Howard Correspondence for Markov's Principle in First-Order Logic and Arithmetic.	TYPES	2016	DBLP DOI BibTeX RDF
32	Bashar Igried, Anton Setzer	Defining Trace Semantics for CSP-Agda.	TYPES	2016	DBLP DOI BibTeX RDF
32	Robin Adams 0001, Marc Bezem, Thierry Coquand	A Normalizing Computation Rule for Propositional Extensionality in Higher-Order Minimal Logic.	TYPES	2016	DBLP DOI BibTeX RDF
32	José Espírito Santo, Maria João Frade, Luís Pinto 0001	Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts.	TYPES	2016	DBLP DOI BibTeX RDF
32	Lukasz Czajka 0001	A Shallow Embedding of Pure Type Systems into First-Order Logic.	TYPES	2016	DBLP DOI BibTeX RDF
32	Auke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, Michael Shulman	Parametricity, Automorphisms of the Universe, and Excluded Middle.	TYPES	2016	DBLP DOI BibTeX RDF
32		Front Matter, Table of Contents, Preface, Conference Organization.	TYPES	2016	DBLP DOI BibTeX RDF
32	Kuen-Bang Hou (Favonia), Robert Harper 0001	Covering Spaces in Homotopy Type Theory.	TYPES	2016	DBLP DOI BibTeX RDF
32	Érik Martin-Dorel, Sergei Soloviev	A Formal Study of Boolean Games with Random Formulas as Payoff Functions.	TYPES	2016	DBLP DOI BibTeX RDF
32	Richard Statman	The Completeness of BCD for an Operational Semantics.	TYPES	2016	DBLP DOI BibTeX RDF
32	Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone	Design and Implementation of the Andromeda Proof Assistant.	TYPES	2016	DBLP DOI BibTeX RDF
32	Dale Miller 0001	Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper).	TYPES	2016	DBLP DOI BibTeX RDF
32	Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau (eds.)	20th International Conference on Types for Proofs and Programs, TYPES 2014, May 12-15, 2014, Paris, France	TYPES	2015	DBLP BibTeX RDF
32	Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg	Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom.	TYPES	2015	DBLP DOI BibTeX RDF
32	Erik Parmann	Functional Kan Simplicial Sets: Non-Constructivity of Exponentiation.	TYPES	2015	DBLP DOI BibTeX RDF
32	Thorsten Altenkirch, Ambrus Kaposi	Towards a Cubical Type Theory without an Interval.	TYPES	2015	DBLP DOI BibTeX RDF
32		Front Matter, Table of Contents, Preface, Externqal Reviewers.	TYPES	2015	DBLP DOI BibTeX RDF
32	Juan Edi, Andrés Viso, Eduardo Bonelli	Efficient Type Checking for Path Polymorphism.	TYPES	2015	DBLP DOI BibTeX RDF
32	Robin Adams 0001, Bart Jacobs 0001	A Type Theory for Probabilistic and Bayesian Reasoning.	TYPES	2015	DBLP DOI BibTeX RDF
32	João Paulo Pizani Flor, Wouter Swierstra, Yorick Sijsling	Pi-Ware: Hardware Description and Verification in Agda.	TYPES	2015	DBLP DOI BibTeX RDF
32	Luca Paolini, Mauro Piccolo, Luca Roversi	A Certified Study of a Reversible Programming Language.	TYPES	2015	DBLP DOI BibTeX RDF