| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Yangyue Feng, Zhaohui Luo |
Typed Operational Semantics for Dependent Record Types  |
TYPES  |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Freek Wiedijk |
Stateless HOL |
TYPES |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Claudio Sacerdoti Coen, Enrico Tassi |
Nonuniform Coercions via Unification Hints |
TYPES |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Tom Hirschowitz (eds.) |
Proceedings Types for Proofs and Programs, Revised Selected Papers |
TYPES |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Asperti, Enrico Tassi |
Superposition as a logical glue |
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 | Marco Gaboardi, Simona Ronchi Della Rocca |
Type Inference for a Polynomial Lambda 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 BibTeX RDF |
|
| 1 | José Espírito Santo, Ralph Matthes, Luis Pinto |
Monadic Translation of Intuitionistic Sequent Calculus. |
TYPES |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhaohui Luo |
Manifest Fields and Module Mechanisms in Intensional Type Theory. |
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 | 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 | Andrea Asperti, Wilmer Ricciotti |
About the Formalization of Some Results by Chebyshev in Number Theory. |
TYPES |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Davide Ancona, Giovanni Lagorio, Elena Zucca |
Type Inference by Coinductive Logic Programming. |
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 | 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 | 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 | 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 | Cezary Kaliszyk, Freek Wiedijk |
Merging Procedural and Declarative Proof. |
TYPES |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Clément Houtmann |
Axiom Directed Focusing. |
TYPES |
2008 |
DBLP DOI BibTeX RDF |
superdeduction, Proof theory, focusing, deduction modulo |
| 1 | Juan Manuel Crespo, Gustavo Betarte, Carlos Luna |
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 | 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 | 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 | Florian Haftmann, Makarius Wenzel |
Local Theory Specifications in Isabelle/Isar. |
TYPES |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Agnieszka Kozubek, Pawel Urzyczyn |
In the Search of a Naive Type Theory. |
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 | Hongwei Xi |
Attributive Types for Proof Erasure. |
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 | Robert Atkey |
CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types. |
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 | Claudio Sacerdoti Coen, Enrico Tassi |
Working with Mathematical Structures in Type Theory. |
TYPES |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan Schwinghammer |
On Normalization by Evaluation for Object Calculi. |
TYPES |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | João Filipe Belo |
Dependently Sorted Logic. |
TYPES |
2007 |
DBLP DOI BibTeX RDF |
|
| 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 | 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 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 | Nathan Whitehead |
A Certified Distributed Security Logic for Authorizing Code. |
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 | Pierre Corbineau |
Deciding Equality in the Constructor 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 | Danko Ilik |
Zermelo's Well-Ordering Theorem in Type Theory. |
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 | Florian Haftmann, Makarius Wenzel |
Constructive Type Classes in Isabelle. |
TYPES |
2006 |
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 BibTeX RDF |
|
| 1 | Herman Geuvers |
(In)consistency of Extensions of Higher Order Logic and Type Theory. |
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 | Maribel Fernández, Murdoch Gabbay |
Curry-Style Types for Nominal Terms. |
TYPES |
2006 |
DBLP DOI BibTeX RDF |
polymorphism, type inference, rewriting, binding |
| 1 | Gilles Dowek |
Truth Values Algebras and Proof Normalization. |
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 | Milad Niqui |
Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers. |
TYPES |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
| 1 | 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 BibTeX RDF |
|
| 1 | Michel Parigot |
On Constructive Existence. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Claudio Sacerdoti Coen |
A Semi-reflexive Tactic for (Sub-)Equational Reasoning. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Morris, Thorsten Altenkirch, Conor McBride |
Exploring the Regular Tree Types. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Meyer, Burkhart Wolff |
Tactic-Based Optimized Compilation of Functional Programs. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexandre Miquel |
lamda-Z: Zermelo's Set Theory as a PTS with 4 Sorts. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Sabrina Tarento |
A Machine-Checked Formalization of the Random Oracle Model. |
TYPES |
2004 |
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 | Markus Michelbrink |
Interfaces as Games, Programs as Strategies. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Fredrik Lindblad, Marcin Benke |
A Tool for Automated Theorem Proving in Agda. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli |
A Content Based Mathematical Search Engine: Whelp. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Grabowski |
Solving Two Problems in General Topology Via Types. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Conor McBride, Healfdene Goguen, James McKinna |
A Few Constructions on Constructors. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Robin Adams |
Formalized Metatheory with Terms Represented by an Indexed Family of Types. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Lionel Elie Mamane |
Surreal Numbers in Coq. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Yves Bertot, Benjamin Grégoire, Xavier Leroy |
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Bove, Thierry Coquand |
Formalising Bitonic Sort in Type Theory. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Berghofer |
Extracting a Normalization Algorithm in Isabelle/HOL. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Sylvain Baro |
Introduction to PAF!, a Proof Assistant for ML Programs Verification. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabio Alessi, Franco Barbanera, Mariangiola Dezani-Ciancaglini |
Tailoring Filter Models. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Berghofer |
A Constructive Proof of Higman's Lemma in Isabelle. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Edwin Brady, Conor McBride, James McKinna |
Inductive Families Need Not Store Their Indices. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 BibTeX RDF |
|
| 1 | Ugo Dal Lago, Simone Martini, Luca Roversi |
Higher-Order Linear Ramified Recurrence. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Furio Honsell, Ivan Scagnetto |
Mobility Types in Coq. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Freek Wiedijk |
Formal Proof Sketches. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Nicola Gambino, Martin Hyland |
Wellfounded Trees and Dependent Polynomial Functors. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Alberto Momigliano, Alwen Fernanto Tiu |
Induction and Co-induction in Sequent Calculus. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Furio Honsell, Marina Lenisa |
"Wave-Style" Geometry of Interaction Models in Rel Are Graph-Like Lambda-Models. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
(linear) graph model, traced monoidal category, weak linear category, categorical geometry of interaction |
| 1 | Sergei Soloviev, David Chemouil |
Some Algebraic Structures in Lambda-Calculus with Inductive Types. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Pierre Corbineau |
First-Order Reasoning in the Calculus of Inductive Constructions. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Kießling, Zhaohui Luo |
Coercions in Hindley-Milner Systems. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Viviana Bono, Jerzy Tiuryn, Pawel Urzyczyn |
Type Inference for Nested Self Types. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Clemens Ballarin |
Locales and Locale Expressions in Isabelle/Isar. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | José Espírito Santo, Luis Pinto |
Confluence and Strong Normalisation of the Generalised Multiary ?-Calculus. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Hongwei Xi |
Applied Type System: Extended Abstract. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Milad Niqui, Yves Bertot |
QArith: Coq Formalisation of Lazy Rational Arithmetic. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvia Ghilezan, Pierre Lescanne |
Classical Proofs, Typed Processes, and Intersection Types: Extended Abstract. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Robin Adams |
A Modular Hierarchy of Logical Frameworks. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker |
A Concurrent Logical Framework: The Propositional Fragment. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Yong Luo, Zhaohui Luo |
Combining Incoherent Coercions for Sigma-Types. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Lorenzo Bettini, Viviana Bono, Silvia Likavec |
A Core Calculus of Higher-Order Mixins and Classes. |
TYPES |
2003 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")