Search results for "types"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
32	Benedikt Ahrens, Ralph Matthes	Heterogeneous Substitution Systems Revisited.	TYPES	2015	DBLP DOI BibTeX RDF
32	Ralph Matthes, Aleksy Schubert (eds.)	19th International Conference on Types for Proofs and Programs, TYPES 2013, April 22-26, 2013, Toulouse, France	TYPES	2014	DBLP BibTeX RDF
32	Olivier Danvy, Chantal Keller, Matthias Puech	Typeful Normalization by Evaluation.	TYPES	2014	DBLP DOI BibTeX RDF
32	Erik Parmann	Investigating Streamless Sets.	TYPES	2014	DBLP DOI BibTeX RDF
32	Maria Emilia Maietti, Samuele Maschio	An Extensional Kleene Realizability Semantics for the Minimalist Foundation.	TYPES	2014	DBLP DOI BibTeX RDF
32	Andrew Polonsky	Extensionality of lambda-*.	TYPES	2014	DBLP DOI BibTeX RDF
32	Ali Assaf 0002	A Calculus of Constructions with Explicit Subtyping.	TYPES	2014	DBLP DOI BibTeX RDF
32	Nicolai Kraus	The General Universal Property of the Propositional Truncation.	TYPES	2014	DBLP DOI BibTeX RDF
32	Aleksy Schubert, Pawel Urzyczyn, Daria Walukiewicz-Chrzaszcz	Restricted Positive Quantification Is Not Elementary.	TYPES	2014	DBLP DOI BibTeX RDF
32		Front Matter, Table of Contents, Preface, Authors Index.	TYPES	2014	DBLP DOI BibTeX RDF
32	Jules Hedges	Dialectica Categories and Games with Bidding.	TYPES	2014	DBLP DOI BibTeX RDF
32	Raphaël Cauderlier, Catherine Dubois	Objects and Subtyping in the Lambda-Pi-Calculus Modulo.	TYPES	2014	DBLP DOI BibTeX RDF
32	Jean-Louis Krivine	On the Structure of Classical Realizability Models of ZF.	TYPES	2014	DBLP DOI BibTeX RDF
32	Sergei Soloviev 0001	On Isomorphism of Dependent Products in a Typed Logical Framework.	TYPES	2014	DBLP DOI BibTeX RDF
32	Silvia Steila	An Intuitionistic Analysis of Size-change Termination.	TYPES	2014	DBLP DOI BibTeX RDF
32	Andrew M. Pitts	Nominal Presentation of Cubical Sets Models of Type Theory.	TYPES	2014	DBLP DOI BibTeX RDF
32	Nils Anders Danielsson, Bengt Nordström (eds.)	18th International Workshop on Types for Proofs and Programs, TYPES 2011, September 8-11, 2011, Bergen, Norway	TYPES	2013	DBLP BibTeX RDF
32	Christian Retoré	The Montagovian Generative Lexicon Lambda Ty_n: a Type Theoretical Framework for Natural Language Semantics.	TYPES	2013	DBLP DOI BibTeX RDF
32	Leonardo Rodríguez, Daniel Fridlender, Miguel Pagano	A Certified Extension of the Krivine Machine for a Call-by-Name Higher-Order Imperative Language.	TYPES	2013	DBLP DOI BibTeX RDF
32	Stefano Berardi, Silvia Steila	Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic.	TYPES	2013	DBLP DOI BibTeX RDF
32	Danel Ahman, Tarmo Uustalu	Update Monads: Cointerpreting Directed Containers.	TYPES	2013	DBLP DOI BibTeX RDF
32	Danko Ilik, Keiko Nakata 0001	A Direct Version of Veldman's Proof of Open Induction on Cantor Space via Delimited Control Operators.	TYPES	2013	DBLP DOI BibTeX RDF
32	Tao Xue	Definitional Extension in Type Theory.	TYPES	2013	DBLP DOI BibTeX RDF
32	Hugo Herbelin, Arnaud Spiwack	The Rooster and the Syntactic Bracket.	TYPES	2013	DBLP DOI BibTeX RDF
32	Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, Carlos Luna 0001	Formally Verified Implementation of an Idealized Model of Virtualization.	TYPES	2013	DBLP DOI BibTeX RDF
32	Joëlle Despeyroux, Kaustuv Chaudhuri	A Hybrid Linear Logic for Constrained Transition Systems.	TYPES	2013	DBLP DOI BibTeX RDF
32	Marc Bezem, Thierry Coquand, Simon Huber	A Model of Type Theory in Cubical Sets.	TYPES	2013	DBLP DOI BibTeX RDF
32		Frontmatter, Table of Contents, Preface, Conference Organization.	TYPES	2013	DBLP DOI BibTeX RDF
32	Ulrich Berger 0001, Monika Seisenberger, Gregory J. M. Woods	Extracting Imperative Programs from Proofs: In-place Quicksort.	TYPES	2013	DBLP DOI BibTeX RDF
32	Federico Aschieri, Margherita Zorzi	A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle.	TYPES	2013	DBLP DOI BibTeX RDF
32	Nils Anders Danielsson, Bengt Nordström	Frontmatter, Table of Contents, Preface, Workshop Organization.	TYPES	2011	DBLP DOI BibTeX RDF
32	Johan Georg Granström	A new approach to the semantics of model diagrams.	TYPES	2011	DBLP DOI BibTeX RDF
32	Aloïs Brunel	Non-constructive complex analysis in Coq.	TYPES	2011	DBLP DOI BibTeX RDF
32	Ralph Matthes, Célia Picard	Verification of redecoration for infinite triangular matrices using coinduction.	TYPES	2011	DBLP DOI BibTeX RDF
32	Cezar Ionescu, Patrik Jansson	Testing versus proving in climate impact research.	TYPES	2011	DBLP DOI BibTeX RDF
32	Jörg Endrullis, Andrew Polonsky	Infinitary Rewriting Coinductively.	TYPES	2011	DBLP DOI BibTeX RDF
32	Tom Hirschowitz (eds.)	Proceedings Types for Proofs and Programs, Revised Selected Papers, TYPES 2009, Aussois, France, 12-15th May 2009.	TYPES	2009	DBLP DOI BibTeX RDF
32	Stefano Berardi, Ferruccio Damiani, Ugo de'Liguoro (eds.)	Types for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers	TYPES	2009	DBLP DOI BibTeX RDF
32	Andrea Asperti, Enrico Tassi	Superposition as a logical glue	TYPES	2009	DBLP DOI BibTeX RDF
32	Freek Wiedijk	Stateless HOL	TYPES	2009	DBLP DOI BibTeX RDF
32	Claudio Sacerdoti Coen, Enrico Tassi	Nonuniform Coercions via Unification Hints	TYPES	2009	DBLP DOI BibTeX RDF
32	Marino Miculan, Ivan Scagnetto, Furio Honsell (eds.)	Types for Proofs and Programs, International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers	TYPES	2008	DBLP DOI BibTeX RDF
32	Amal Ahmed 0001, Nick Benton, Martin Hofmann 0001, Greg Morrisett	08061 Abstracts Collection -- Types, Logics and Semantics for State.	Types, Logics and Semantics for State	2008	DBLP BibTeX RDF
32	Amal Ahmed 0001, Nick Benton, Martin Hofmann 0001, Greg Morrisett	08061 Executive Summary -- Types, Logics and Semantics for State.	Types, Logics and Semantics for State	2008	DBLP BibTeX RDF
32	Zhaohui Luo	Manifest Fields and Module Mechanisms in Intensional Type Theory.	TYPES	2008	DBLP DOI BibTeX RDF
32	Luca Paolini, Mauro Piccolo	A Process-Model for Linear Programs.	TYPES	2008	DBLP DOI BibTeX RDF
32	Eelis van der Weegen, James McKinna	A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq.	TYPES	2008	DBLP DOI BibTeX RDF
32	Marco Gaboardi, Simona Ronchi Della Rocca	Type Inference for a Polynomial Lambda Calculus.	TYPES	2008	DBLP DOI BibTeX RDF
32	Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini	A New Elimination Rule for the Calculus of Inductive Constructions.	TYPES	2008	DBLP DOI BibTeX RDF
32	Juan Manuel Crespo, Gustavo Betarte, Carlos Luna 0001	A Framework for the Analysis of Access Control Models for Interactive Mobile Devices.	TYPES	2008	DBLP DOI BibTeX RDF	mobile devices, Access control models, formal proofs
32	Andrea Asperti, Wilmer Ricciotti	About the Formalization of Some Results by Chebyshev in Number Theory.	TYPES	2008	DBLP DOI BibTeX RDF
32	Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, Roel C. de Vrijer	Proving Infinitary Normalization.	TYPES	2008	DBLP DOI BibTeX RDF
32	Milad Niqui	Coalgebraic Reasoning in Coq: Bisimulation and the lambda-Coiteration Scheme.	TYPES	2008	DBLP DOI BibTeX RDF	Coiteration, Bisimulation, Coalgebra, Coq, Coinduction
32	Florian Haftmann, Makarius Wenzel	Local Theory Specifications in Isabelle/Isar.	TYPES	2008	DBLP DOI BibTeX RDF
32	Davide Ancona, Giovanni Lagorio, Elena Zucca	Type Inference by Coinductive Logic Programming.	TYPES	2008	DBLP DOI BibTeX RDF
32	Luca Roversi, Luca Vercelli	Some Complexity and Expressiveness Results on Multimodal and Stratified Proof Nets.	TYPES	2008	DBLP DOI BibTeX RDF	Structural Proof-theory, Polynomial Time Computations, Linear Logic, Implicit Computational Complexity
32	Clément Houtmann	Axiom Directed Focusing.	TYPES	2008	DBLP DOI BibTeX RDF	superdeduction, Proof theory, focusing, deduction modulo
32	Dag Hovland	A Type System for Usage of Software Components.	TYPES	2008	DBLP DOI BibTeX RDF	Component Usage, Process Model, Type System, Parallel Execution, Component Software
32	Cezary Kaliszyk, Freek Wiedijk	Merging Procedural and Declarative Proof.	TYPES	2008	DBLP DOI BibTeX RDF
32	Thorsten Altenkirch, Conor McBride (eds.)	Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers	TYPES	2007	DBLP DOI BibTeX RDF
32	João Filipe Belo	Dependently Sorted Logic.	TYPES	2007	DBLP DOI BibTeX RDF
32	Rasmus Ejlers Møgelberg, Alex Simpson	A Logic for Parametric Polymorphism with Effects.	TYPES	2007	DBLP DOI BibTeX RDF
32	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
32	Ralph Matthes, Martin Strecker	Verification of the Redecoration Algorithm for Triangular Matrices.	TYPES	2007	DBLP DOI BibTeX RDF
32	Lisa Allali	Algorithmic Equality in Heyting Arithmetic Modulo.	TYPES	2007	DBLP DOI BibTeX RDF
32	Pierre Corbineau	A Declarative Language for the Coq Proof Assistant.	TYPES	2007	DBLP DOI BibTeX RDF
32	Antoine Genitrini, Jakub Kozik, Marek Zaionc	Intuitionistic vs. Classical Tautologies, Quantitative Comparison.	TYPES	2007	DBLP DOI BibTeX RDF
32	Jean-Christophe Filliâtre, Christine Paulin-Mohring, Benjamin Werner (eds.)	Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers	TYPES	2006	DBLP DOI BibTeX RDF
32	Pierre Corbineau	Deciding Equality in the Constructor Theory.	TYPES	2006	DBLP DOI BibTeX RDF
32	Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli	Crafting a Proof Assistant.	TYPES	2006	DBLP DOI BibTeX RDF
32	Florent Kirchner	A Finite First-Order Theory of Classes.	TYPES	2006	DBLP DOI BibTeX RDF
32	Danko Ilik	Zermelo's Well-Ordering Theorem in Type Theory.	TYPES	2006	DBLP DOI BibTeX RDF
32	Frédéric Besson	Fast Reflexive Arithmetic Tactics the Linear Case and Beyond.	TYPES	2006	DBLP DOI BibTeX RDF
32	Richard Bonichon, Olivier Hermant	On Constructive Cut Admissibility in Deduction Modulo.	TYPES	2006	DBLP DOI BibTeX RDF
32	Nathan Whitehead	A Certified Distributed Security Logic for Authorizing Code.	TYPES	2006	DBLP DOI BibTeX RDF
32	Herman Geuvers	(In)consistency of Extensions of Higher Order Logic and Type Theory.	TYPES	2006	DBLP DOI BibTeX RDF
32	Robin Adams 0001, 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
32	Venanzio Capretta, Amy P. Felty	Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq.	TYPES	2006	DBLP DOI BibTeX RDF
32	Gilles Dowek	Truth Values Algebras and Proof Normalization.	TYPES	2006	DBLP DOI BibTeX RDF
32	Nils Anders Danielsson	A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family.	TYPES	2006	DBLP DOI BibTeX RDF
32	Stefano Berardi, Mario Coppo, Ferruccio Damiani (eds.)	Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers	TYPES	2004	DBLP DOI BibTeX RDF
32	Solange Coupet-Grimal, William Delobel	A Uniform and Certified Approach for Two Static Analyses.	TYPES	2004	DBLP DOI BibTeX RDF
32	Michel Parigot	On Constructive Existence.	TYPES	2004	DBLP DOI BibTeX RDF
32	Yves Bertot, Benjamin Grégoire, Xavier Leroy	A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis.	TYPES	2004	DBLP DOI BibTeX RDF
32	Thomas Meyer 0001, Burkhart Wolff	Tactic-Based Optimized Compilation of Functional Programs.	TYPES	2004	DBLP DOI BibTeX RDF
32	Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli	A Content Based Mathematical Search Engine: Whelp.	TYPES	2004	DBLP DOI BibTeX RDF
32	Claudio Sacerdoti Coen	A Semi-reflexive Tactic for (Sub-)Equational Reasoning.	TYPES	2004	DBLP DOI BibTeX RDF
32	Lionel Elie Mamane	Surreal Numbers in Coq.	TYPES	2004	DBLP DOI BibTeX RDF
32	Gilles Barthe, Sabrina Tarento	A Machine-Checked Formalization of the Random Oracle Model.	TYPES	2004	DBLP DOI BibTeX RDF
32	Fredrik Lindblad, Marcin Benke	A Tool for Automated Theorem Proving in Agda.	TYPES	2004	DBLP DOI BibTeX RDF
32	Conor McBride, Healfdene Goguen, James McKinna	A Few Constructions on Constructors.	TYPES	2004	DBLP DOI BibTeX RDF
32	Alexandre Miquel	lamda-Z: Zermelo's Set Theory as a PTS with 4 Sorts.	TYPES	2004	DBLP DOI BibTeX RDF
32	Markus Michelbrink	Interfaces as Games, Programs as Strategies.	TYPES	2004	DBLP DOI BibTeX RDF
32	Herman Geuvers, Freek Wiedijk (eds.)	Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers	TYPES	2003	DBLP DOI BibTeX RDF
32	Stefan Berghofer	A Constructive Proof of Higman's Lemma in Isabelle.	TYPES	2003	DBLP DOI BibTeX RDF
32	Jacek Chrzaszcz	Modules in Coq Are and Will Be Correct.	TYPES	2003	DBLP DOI BibTeX RDF
32	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
32	Clemens Ballarin	Locales and Locale Expressions in Isabelle/Isar.	TYPES	2003	DBLP DOI BibTeX RDF
32	Freek Wiedijk	Formal Proof Sketches.	TYPES	2003	DBLP DOI BibTeX RDF
32	Robin Adams 0001	A Modular Hierarchy of Logical Frameworks.	TYPES	2003	DBLP DOI BibTeX RDF