Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Jan M. Smith
@incollection{DBLP:series/leus/Smith12,
author = {Jan M. Smith},
editor = {Peter Dybjer and
Sten Lindstr{\"{o}}m and
Erik Palmgren and
G{\"{o}}ran Sundholm},
title = {Evolution and Logic},
booktitle = {Epistemology versus Ontology - Essays on the Philosophy and Foundations
of Mathematics in Honour of Per Martin-L{\"{o}}f},
series = {Logic, Epistemology, and the Unity of Science},
volume = {27},
pages = {129--138},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-94-007-4435-6\_6},
doi = {10.1007/978-94-007-4435-6\_6},
timestamp = {Sun, 02 Jun 2019 20:42:14 +0200},
biburl = {https://dblp.org/rec/series/leus/Smith12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/apal/CoquandSSV03,
author = {Thierry Coquand and
Giovanni Sambin and
Jan M. Smith and
Silvio Valentini},
title = {Inductively generated formal topologies},
journal = {Ann. Pure Appl. Log.},
volume = {124},
number = {1-3},
pages = {71--106},
year = {2003},
url = {https://doi.org/10.1016/S0168-0072(03)00052-6},
doi = {10.1016/S0168-0072(03)00052-6},
timestamp = {Fri, 21 Feb 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/apal/CoquandSSV03.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/CoquandSSS00,
author = {Thierry Coquand and
Sara Sadocco and
Giovanni Sambin and
Jan M. Smith},
title = {Formal Topologies on The Set of First-Order Formulae},
journal = {J. Symb. Log.},
volume = {65},
number = {3},
pages = {1183--1192},
year = {2000},
url = {https://doi.org/10.2307/2586694},
doi = {10.2307/2586694},
timestamp = {Sun, 28 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/CoquandSSS00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/types/1999,
editor = {Thierry Coquand and
Peter Dybjer and
Bengt Nordstr{\"{o}}m and
Jan M. Smith},
title = {Types for Proofs and Programs, International Workshop TYPES'99, L{\"{o}}keberg,
Sweden, June 12-16, 1999, Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {1956},
publisher = {Springer},
year = {2000},
url = {https://doi.org/10.1007/3-540-44557-9},
doi = {10.1007/3-540-44557-9},
isbn = {3-540-41517-3},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/types/1999.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/logcom/TammetS98,
author = {Tanel Tammet and
Jan M. Smith},
title = {Optimized Encodings of Fragments of Type Theory in First-Order Logic},
journal = {J. Log. Comput.},
volume = {8},
number = {6},
pages = {713--744},
year = {1998},
url = {https://doi.org/10.1093/logcom/8.6.713},
doi = {10.1093/LOGCOM/8.6.713},
timestamp = {Wed, 17 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/logcom/TammetS98.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/types/CoquandS95,
author = {Thierry Coquand and
Jan M. Smith},
editor = {Stefano Berardi and
Mario Coppo},
title = {An Application of Constructive Completeness},
booktitle = {Types for Proofs and Programs, International Workshop TYPES'95, Torino,
Italy, June 5-8, 1995, Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {1158},
pages = {76--84},
publisher = {Springer},
year = {1995},
url = {https://doi.org/10.1007/3-540-61780-9\_63},
doi = {10.1007/3-540-61780-9\_63},
timestamp = {Tue, 14 May 2019 10:00:42 +0200},
biburl = {https://dblp.org/rec/conf/types/CoquandS95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/types/TammetS95,
author = {Tanel Tammet and
Jan M. Smith},
editor = {Stefano Berardi and
Mario Coppo},
title = {Optimized Encodings of Fragments of Type Theory in First Order Logic},
booktitle = {Types for Proofs and Programs, International Workshop TYPES'95, Torino,
Italy, June 5-8, 1995, Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {1158},
pages = {265--287},
publisher = {Springer},
year = {1995},
url = {https://doi.org/10.1007/3-540-61780-9\_75},
doi = {10.1007/3-540-61780-9\_75},
timestamp = {Sun, 21 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/types/TammetS95.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/types/1994,
editor = {Peter Dybjer and
Bengt Nordstr{\"{o}}m and
Jan M. Smith},
title = {Types for Proofs and Programs, International Workshop TYPES'94, B{\aa}stad,
Sweden, June 6-10, 1994, Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {996},
publisher = {Springer},
year = {1995},
url = {https://doi.org/10.1007/3-540-60579-7},
doi = {10.1007/3-540-60579-7},
isbn = {3-540-60579-7},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/types/1994.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/eatcs/CoquandNSS94,
author = {Thierry Coquand and
Bengt Nordstr{\"{o}}m and
Jan M. Smith and
Bj{\"{o}}rn von Sydow},
title = {Type Theorie Programming},
journal = {Bull. {EATCS}},
volume = {52},
pages = {203--228},
year = {1994},
timestamp = {Thu, 18 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/eatcs/CoquandNSS94.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/csl/Smith92,
author = {Jan M. Smith},
editor = {Egon B{\"{o}}rger and
Gerhard J{\"{a}}ger and
Hans Kleine B{\"{u}}ning and
Simone Martini and
Michael M. Richter},
title = {Kleene's Slash and Existence of Values of Open Terms in Type Theory},
booktitle = {Computer Science Logic, 6th Workshop, {CSL} '92, San Miniato, Italy,
September 28 - October 2, 1992, Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {702},
pages = {395--402},
publisher = {Springer},
year = {1992},
url = {https://doi.org/10.1007/3-540-56992-8\_23},
doi = {10.1007/3-540-56992-8\_23},
timestamp = {Fri, 17 Jul 2020 16:12:45 +0200},
biburl = {https://dblp.org/rec/conf/csl/Smith92.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{DBLP:conf/balt/MintsST91,
author = {Grigori Mints and
Jan M. Smith and
Enn Tyugu},
editor = {Janis Barzdins and
Dines Bj{\o}rner},
title = {Type-theoretical Semantics of Some Declarative Languages},
booktitle = {Baltic Computer Science, Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {502},
pages = {18--32},
publisher = {Springer},
year = {1991},
url = {https://doi.org/10.1007/BFb0019354},
doi = {10.1007/BFB0019354},
timestamp = {Tue, 14 May 2019 10:00:53 +0200},
biburl = {https://dblp.org/rec/conf/balt/MintsST91.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/ndjfl/Smith89,
author = {Jan M. Smith},
title = {Propositional Functions and Families of Types},
journal = {Notre Dame J. Formal Log.},
volume = {30},
number = {3},
pages = {442--458},
year = {1989},
url = {https://doi.org/10.1305/ndjfl/1093635159},
doi = {10.1305/NDJFL/1093635159},
timestamp = {Thu, 21 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/ndjfl/Smith89.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/Smith88,
author = {Jan M. Smith},
title = {The Independence of Peano's Fourth Axiom from Martin-Lof's Type Theory
Without Universes},
journal = {J. Symb. Log.},
volume = {53},
number = {3},
pages = {840--845},
year = {1988},
url = {https://doi.org/10.2307/2274575},
doi = {10.2307/2274575},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/Smith88.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/SalvesenS88,
author = {Anne Salvesen and
Jan M. Smith},
title = {The Strength of the Subset Type in Martin-L{\"{o}}f's Type Theory},
booktitle = {Proceedings of the Third Annual Symposium on Logic in Computer Science
{(LICS} '88), Edinburgh, Scotland, UK, July 5-8, 1988},
pages = {384--391},
publisher = {{IEEE} Computer Society},
year = {1988},
url = {https://doi.org/10.1109/LICS.1988.5135},
doi = {10.1109/LICS.1988.5135},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/SalvesenS88.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/cl/PeterssonS86,
author = {Kent Petersson and
Jan M. Smith},
title = {Program Derivation in Type Theory: {A} Partitioning Problem},
journal = {Comput. Lang.},
volume = {11},
number = {3/4},
pages = {161--172},
year = {1986},
url = {https://doi.org/10.1016/0096-0551(86)90009-3},
doi = {10.1016/0096-0551(86)90009-3},
timestamp = {Thu, 18 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/cl/PeterssonS86.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/bit/NordstromS84,
author = {Bengt Nordstr{\"{o}}m and
Jan M. Smith},
title = {Propositions and Specifications of Programs in Martin-L{\"{o}}fs
Type Theory},
journal = {{BIT}},
volume = {24},
number = {3},
pages = {288--301},
year = {1984},
url = {https://doi.org/10.1007/BF02136027},
doi = {10.1007/BF02136027},
timestamp = {Tue, 22 Jun 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/bit/NordstromS84.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jsyml/Smith84a,
author = {Jan M. Smith},
title = {An Interpretation of Martin-Lof's Type Theory in a Type-Free Theory
of Propositions},
journal = {J. Symb. Log.},
volume = {49},
number = {3},
pages = {730--753},
year = {1984},
url = {https://doi.org/10.2307/2274128},
doi = {10.2307/2274128},
timestamp = {Sun, 28 May 2017 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jsyml/Smith84a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fct/Smith83,
author = {Jan M. Smith},
editor = {Marek Karpinski},
title = {The Identification of Propositions and types in Martin-L{\"{o}}f's
Type Theory: {A} Programming Example},
booktitle = {Fundamentals of Computation Theory, Proceedings of the 1983 International
FCT-Conference, Borgholm, Sweden, August 21-27, 1983},
series = {Lecture Notes in Computer Science},
volume = {158},
pages = {445--456},
publisher = {Springer},
year = {1983},
url = {https://doi.org/10.1007/3-540-12689-9\_125},
doi = {10.1007/3-540-12689-9\_125},
timestamp = {Tue, 14 May 2019 10:00:53 +0200},
biburl = {https://dblp.org/rec/conf/fct/Smith83.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-04-21 17:08 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
