Search results for "TYPES"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	João Paulo Pizani Flor, Wouter Swierstra, Yorick Sijsling	Pi-Ware: Hardware Description and Verification in Agda.	TYPES	2015	DBLP DOI BibTeX RDF
1	Luca Paolini, Mauro Piccolo, Luca Roversi	A Certified Study of a Reversible Programming Language.	TYPES	2015	DBLP DOI BibTeX RDF
1	Benedikt Ahrens, Ralph Matthes	Heterogeneous Substitution Systems Revisited.	TYPES	2015	DBLP DOI BibTeX RDF
1	Olivier Danvy, Chantal Keller, Matthias Puech	Typeful Normalization by Evaluation.	TYPES	2014	DBLP DOI BibTeX RDF
1	Erik Parmann	Investigating Streamless Sets.	TYPES	2014	DBLP DOI BibTeX RDF
1	Maria Emilia Maietti, Samuele Maschio	An Extensional Kleene Realizability Semantics for the Minimalist Foundation.	TYPES	2014	DBLP DOI BibTeX RDF
1	Andrew Polonsky	Extensionality of lambda-*.	TYPES	2014	DBLP DOI BibTeX RDF
1	Ali Assaf 0002	A Calculus of Constructions with Explicit Subtyping.	TYPES	2014	DBLP DOI BibTeX RDF
1	Nicolai Kraus	The General Universal Property of the Propositional Truncation.	TYPES	2014	DBLP DOI BibTeX RDF
1	Aleksy Schubert, Pawel Urzyczyn, Daria Walukiewicz-Chrzaszcz	Restricted Positive Quantification Is Not Elementary.	TYPES	2014	DBLP DOI BibTeX RDF
1	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
1		Front Matter, Table of Contents, Preface, Authors Index.	TYPES	2014	DBLP DOI BibTeX RDF
1	Jules Hedges	Dialectica Categories and Games with Bidding.	TYPES	2014	DBLP DOI BibTeX RDF
1	Raphaël Cauderlier, Catherine Dubois	Objects and Subtyping in the Lambda-Pi-Calculus Modulo.	TYPES	2014	DBLP DOI BibTeX RDF
1	Jean-Louis Krivine	On the Structure of Classical Realizability Models of ZF.	TYPES	2014	DBLP DOI BibTeX RDF
1	Sergei Soloviev 0001	On Isomorphism of Dependent Products in a Typed Logical Framework.	TYPES	2014	DBLP DOI BibTeX RDF
1	Silvia Steila	An Intuitionistic Analysis of Size-change Termination.	TYPES	2014	DBLP DOI BibTeX RDF
1	Andrew M. Pitts	Nominal Presentation of Cubical Sets Models of Type Theory.	TYPES	2014	DBLP DOI BibTeX RDF
1	Benedikt Ahrens, Régis Spadotti	Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory.	TYPES	2014	DBLP DOI BibTeX RDF
1	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
1	Christian Retoré	The Montagovian Generative Lexicon Lambda Ty_n: a Type Theoretical Framework for Natural Language Semantics.	TYPES	2013	DBLP DOI BibTeX RDF
1	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
1	Stefano Berardi, Silvia Steila	Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic.	TYPES	2013	DBLP DOI BibTeX RDF
1	Danel Ahman, Tarmo Uustalu	Update Monads: Cointerpreting Directed Containers.	TYPES	2013	DBLP DOI BibTeX RDF
1	Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, Maddalena Zacchi	Isomorphism of "Functional" Intersection Types.	TYPES	2013	DBLP DOI BibTeX RDF
1	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
1	Tao Xue	Definitional Extension in Type Theory.	TYPES	2013	DBLP DOI BibTeX RDF
1	Hugo Herbelin, Arnaud Spiwack	The Rooster and the Syntactic Bracket.	TYPES	2013	DBLP DOI BibTeX RDF
1	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
1	Joëlle Despeyroux, Kaustuv Chaudhuri	A Hybrid Linear Logic for Constrained Transition Systems.	TYPES	2013	DBLP DOI BibTeX RDF
1	Marc Bezem, Thierry Coquand, Simon Huber	A Model of Type Theory in Cubical Sets.	TYPES	2013	DBLP DOI BibTeX RDF
1		Frontmatter, Table of Contents, Preface, Conference Organization.	TYPES	2013	DBLP DOI BibTeX RDF
1	Ulrich Berger 0001, Monika Seisenberger, Gregory J. M. Woods	Extracting Imperative Programs from Proofs: In-place Quicksort.	TYPES	2013	DBLP DOI BibTeX RDF
1	Federico Aschieri, Margherita Zorzi	A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle.	TYPES	2013	DBLP DOI BibTeX RDF
1	Nils Anders Danielsson, Bengt Nordström	Frontmatter, Table of Contents, Preface, Workshop Organization.	TYPES	2011	DBLP DOI BibTeX RDF
1	Johan Georg Granström	A new approach to the semantics of model diagrams.	TYPES	2011	DBLP DOI BibTeX RDF
1	Aloïs Brunel	Non-constructive complex analysis in Coq.	TYPES	2011	DBLP DOI BibTeX RDF
1	Ralph Matthes, Célia Picard	Verification of redecoration for infinite triangular matrices using coinduction.	TYPES	2011	DBLP DOI BibTeX RDF
1	Cezar Ionescu, Patrik Jansson	Testing versus proving in climate impact research.	TYPES	2011	DBLP DOI BibTeX RDF
1	Jörg Endrullis, Andrew Polonsky	Infinitary Rewriting Coinductively.	TYPES	2011	DBLP DOI BibTeX RDF
1	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
1	Andrea Asperti, Enrico Tassi	Superposition as a logical glue	TYPES	2009	DBLP DOI BibTeX RDF
1	Freek Wiedijk	Stateless HOL	TYPES	2009	DBLP DOI BibTeX RDF
1	Yangyue Feng, Zhaohui Luo	Typed Operational Semantics for Dependent Record Types	TYPES	2009	DBLP DOI BibTeX RDF
1	Claudio Sacerdoti Coen, Enrico Tassi	Nonuniform Coercions via Unification Hints	TYPES	2009	DBLP DOI BibTeX RDF
1	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
1	Zhaohui Luo	Manifest Fields and Module Mechanisms in Intensional Type Theory.	TYPES	2008	DBLP DOI BibTeX RDF
1	Luca Paolini, Mauro Piccolo	A Process-Model for Linear Programs.	TYPES	2008	DBLP DOI BibTeX RDF
1	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
1	Marco Gaboardi, Simona Ronchi Della Rocca	Type Inference for a Polynomial Lambda Calculus.	TYPES	2008	DBLP DOI BibTeX RDF
1	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
1	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
1	José Espírito Santo, Ralph Matthes, Luís Pinto 0001	Monadic Translation of Intuitionistic Sequent Calculus.	TYPES	2008	DBLP DOI BibTeX RDF
1	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
1	Erik Ernst	First-Class Object Sets.	TYPES	2008	DBLP DOI BibTeX RDF	Object sets, multi-object method calls, composition, types
1	Camillo Fiorentini, Alberto Momigliano, Mario Ornaghi	Towards a Type Discipline for Answer Set Programming.	TYPES	2008	DBLP DOI BibTeX RDF	many sorted interpretation, type checking, Answer set programming, grounding
1	Andrea Asperti, Wilmer Ricciotti	About the Formalization of Some Results by Chebyshev in Number Theory.	TYPES	2008	DBLP DOI BibTeX RDF
1	Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, Roel C. de Vrijer	Proving Infinitary Normalization.	TYPES	2008	DBLP DOI BibTeX RDF
1	Milad Niqui	Coalgebraic Reasoning in Coq: Bisimulation and the lambda-Coiteration Scheme.	TYPES	2008	DBLP DOI BibTeX RDF	Coiteration, Bisimulation, Coalgebra, Coq, Coinduction
1	Florian Haftmann, Makarius Wenzel	Local Theory Specifications in Isabelle/Isar.	TYPES	2008	DBLP DOI BibTeX RDF
1	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
1	Davide Ancona, Giovanni Lagorio, Elena Zucca	Type Inference by Coinductive Logic Programming.	TYPES	2008	DBLP DOI BibTeX RDF
1	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
1	Clément Houtmann	Axiom Directed Focusing.	TYPES	2008	DBLP DOI BibTeX RDF	superdeduction, Proof theory, focusing, deduction modulo
1	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
1	Cezary Kaliszyk, Freek Wiedijk	Merging Procedural and Declarative Proof.	TYPES	2008	DBLP DOI BibTeX RDF
1	João Filipe Belo	Dependently Sorted Logic.	TYPES	2007	DBLP DOI BibTeX RDF
1	Jan Schwinghammer	On Normalization by Evaluation for Object Calculi.	TYPES	2007	DBLP DOI BibTeX RDF
1	Claudio Sacerdoti Coen, Enrico Tassi	Working with Mathematical Structures in Type Theory.	TYPES	2007	DBLP DOI BibTeX RDF
1	Rasmus Ejlers Møgelberg, Alex Simpson	A Logic for Parametric Polymorphism with Effects.	TYPES	2007	DBLP DOI BibTeX RDF
1	Agnieszka Kozubek, Pawel Urzyczyn	In the Search of a Naive Type Theory.	TYPES	2007	DBLP DOI BibTeX RDF
1	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
1	Ralph Matthes, Martin Strecker	Verification of the Redecoration Algorithm for Triangular Matrices.	TYPES	2007	DBLP DOI BibTeX RDF
1	Lisa Allali	Algorithmic Equality in Heyting Arithmetic Modulo.	TYPES	2007	DBLP DOI BibTeX RDF
1	Pierre Corbineau	A Declarative Language for the Coq Proof Assistant.	TYPES	2007	DBLP DOI BibTeX RDF
1	Antoine Genitrini, Jakub Kozik, Marek Zaionc	Intuitionistic vs. Classical Tautologies, Quantitative Comparison.	TYPES	2007	DBLP DOI BibTeX RDF
1	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
1	Hongwei Xi	Attributive Types for Proof Erasure.	TYPES	2007	DBLP DOI BibTeX RDF
1	Robert Atkey	CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types.	TYPES	2007	DBLP DOI BibTeX RDF
1	José Espírito Santo, Silvia Ghilezan, Jelena Ivetic	Characterising Strongly Normalising Intuitionistic Sequent Terms.	TYPES	2007	DBLP DOI BibTeX RDF
1	Hugo R. Simões, Kevin Hammond, Mário Florido, Pedro B. Vasconcelos	Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs.	TYPES	2006	DBLP DOI BibTeX RDF
1	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
1	Pierre Corbineau	Deciding Equality in the Constructor Theory.	TYPES	2006	DBLP DOI BibTeX RDF
1	Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli	Crafting a Proof Assistant.	TYPES	2006	DBLP DOI BibTeX RDF
1	Florent Kirchner	A Finite First-Order Theory of Classes.	TYPES	2006	DBLP DOI BibTeX RDF
1	Danko Ilik	Zermelo's Well-Ordering Theorem in Type Theory.	TYPES	2006	DBLP DOI BibTeX RDF
1	Frédéric Besson	Fast Reflexive Arithmetic Tactics the Linear Case and Beyond.	TYPES	2006	DBLP DOI BibTeX RDF
1	Richard Bonichon, Olivier Hermant	On Constructive Cut Admissibility in Deduction Modulo.	TYPES	2006	DBLP DOI BibTeX RDF
1	Nathan Whitehead	A Certified Distributed Security Logic for Authorizing Code.	TYPES	2006	DBLP DOI BibTeX RDF
1	Herman Geuvers	(In)consistency of Extensions of Higher Order Logic and Type Theory.	TYPES	2006	DBLP DOI BibTeX RDF
1	Maribel Fernández, Murdoch Gabbay	Curry-Style Types for Nominal Terms.	TYPES	2006	DBLP DOI BibTeX RDF	polymorphism, type inference, rewriting, binding
1	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
1	Florian Haftmann, Makarius Wenzel	Constructive Type Classes in Isabelle.	TYPES	2006	DBLP DOI BibTeX RDF
1	Matthieu Sozeau	Subset Coercions in Coq.	TYPES	2006	DBLP DOI BibTeX RDF
1	Venanzio Capretta, Amy P. Felty	Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq.	TYPES	2006	DBLP DOI BibTeX RDF
1	Gilles Dowek	Truth Values Algebras and Proof Normalization.	TYPES	2006	DBLP DOI BibTeX RDF
1	Milad Niqui	Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers.	TYPES	2006	DBLP DOI BibTeX RDF
1	Nils Anders Danielsson	A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family.	TYPES	2006	DBLP DOI BibTeX RDF
1	Solange Coupet-Grimal, William Delobel	A Uniform and Certified Approach for Two Static Analyses.	TYPES	2004	DBLP DOI BibTeX RDF
1	Stefan Berghofer	Extracting a Normalization Algorithm in Isabelle/HOL.	TYPES	2004	DBLP DOI BibTeX RDF

Publications at "TYPES"( http://dblp.L3S.de/Venues/TYPES )