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 |
|