Inductively generated formal topologies T Coquand, G Sambin, J Smith, S Valentini Annals of Pure and Applied Logic 124 (1-3), 71-106, 2003 | 141 | 2003 |

The modal logic of provability. The sequential approach G Sambin, S Valentini Journal of Philosophical Logic 11 (3), 311-342, 1982 | 99 | 1982 |

Building up a toolbox for Martin-Löf's type theory: subset theory P Martin-Löf Twenty five years of Constructive Type Theory 36, 221, 1998 | 82 | 1998 |

The modal logic of provability: cut-elimination S Valentini Journal of Philosophical logic 12 (4), 471-476, 1983 | 72 | 1983 |

Constructive domain theory as a branch of intuitionistic pointfree topology G Sambin, S Valentini, P Virgili Theoretical Computer Science 159 (2), 319-341, 1996 | 48 | 1996 |

Twenty five years of constructive type theory G Sambin, JM Smith Oxford University Press, 1998 | 44 | 1998 |

A modal sequent calculus for a fragment of arithmetic G Sambin, S Valentini Studia Logica 39 (2-3), 245-256, 1980 | 40 | 1980 |

Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory? ME Maietti, S Valentini Mathematical Logic Quarterly 45 (4), 521-532, 1999 | 30 | 1999 |

Tychonoff's theorem in the framework of formal topologies S Negri, S Valentini The Journal of Symbolic Logic 62 (4), 1315-1332, 1997 | 27 | 1997 |

A structural investigation on formal topology: coreflection of formal covers and exponentiability ME Maietti, S Valentini Journal of Symbolic Logic, 967-1005, 2004 | 21 | 2004 |

An elementary proof of strong normalization for intersection types S Valentini Archive for Mathematical Logic 40 (7), 475-488, 2001 | 19 | 2001 |

The problem of the formalization of constructive topology S Valentini Archive for Mathematical Logic 44 (1), 115-129, 2005 | 16 | 2005 |

The sequent calculus for the modal logic D S Valentini Unione Matematica Italiana. Bollettino. A. Serie 7 (7), 3, 1993 | 14 | 1993 |

A general method for proving the normalization theorem for first and second order typed λ-calculi V Capretta, S Valentini Mathematical Structures in Computer Science 9 (6), 719-739, 1999 | 13 | 1999 |

Representation theorems for quantales S Valentini Mathematical Logic Quarterly 40 (2), 182-190, 1994 | 13 | 1994 |

Vagueness, Kant and topology: A study of formal epistemology G Boniolo, S Valentini Journal of Philosophical Logic 37 (2), 141, 2008 | 12 | 2008 |

The forget-restore principle: a paradigmatic example S Valentini Twenty Five Years of Constructive Type Theory 36, 275, 1998 | 12 | 1998 |

Decidability in Intuitionistic Type Theory is functionally decidable S Valentini Mathematical Logic Quarterly 42 (1), 300-304, 1996 | 12 | 1996 |

Krivine's intuitionistic proof of classical completeness (for countable languages) S Berardi, S Valentini Annals of Pure and Applied Logic 129 (1-3), 93-106, 2004 | 11 | 2004 |

Building up a tool-box for Martin-Löf intuitionistic type theory G Sambin, S Valentini to appear, 1998 | 10 | 1998 |