Zobrazeno 1 - 10
of 21
pro vyhledávání: '"Stefan Berghofer"'
Autor:
Stefan Berghofer
Publikováno v:
Journal of Automated Reasoning. 49:303-326
We present a solution to the PoplMark challenge designed by Aydemir et al., which has as a goal the formalization of the meta-theory of System \(\hbox{F}_{
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::327019ff4594ee5ffb329efe2a256662
https://doi.org/10.1007/s10817-011-9231-4
https://doi.org/10.1007/s10817-011-9231-4
Publikováno v:
LICS
LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LF's judgments. Althoug
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e91cbe8a980712c68a82e144e7c47236
https://doi.org/10.1145/1877714.1877721
https://doi.org/10.1145/1877714.1877721
Autor:
Stefan Berghofer, Christian Urban
Publikováno v:
Electronic Notes in Theoretical Computer Science. 174(5):53-67
Often debates about pros and cons of various techniques for formalising lambda-calculi rely on subjective arguments, such as de Bruijn indices are hard to read for humans or nominal approaches come close to the style of reasoning employed in informal
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1f0ad8e4eae6ac1484b45e76f1d9971c
Publikováno v:
Programming Languages and Systems ISBN: 9783642253171
APLAS
APLAS
We investigate how to add coercive structural subtyping to a type system for simply-typed lambda calculus with Hindley-Milner polymorphism. Coercions allow to convert between different types, and their automatic insertion can greatly increase readabi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::08037dd2e27a3a02cf314f54880bd4d2
https://doi.org/10.1007/978-3-642-25318-8_10
https://doi.org/10.1007/978-3-642-25318-8_10
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642033582
TPHOLs
TPHOLs
Inductively defined predicates are frequently used in formal specifications. Using the theorem prover Isabelle , we describe an approach to turn a class of systems of inductively defined predicates into a system of equations using data flow analysis;
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d0e74f64c50656f53bd2e4b0e6e9e830
https://doi.org/10.1007/978-3-642-03359-9_11
https://doi.org/10.1007/978-3-642-03359-9_11
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642033582
Theorem Proving in Higher Order Logics
Theorem Proving in Higher Order Logics
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9be0ca1a23f5a2e51bd7f639177ed120
https://doi.org/10.1007/978-3-642-03359-9
https://doi.org/10.1007/978-3-642-03359-9
Autor:
Markus Reiter, Stefan Berghofer
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642033582
TPHOLs
TPHOLs
This paper presents a formalization of a library for automata on bit strings in the theorem prover Isabelle/HOL. It forms the basis of a reflection-based decision procedure for Presburger arithmetic, which is efficiently executable thanks to Isabelle
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a63616581ecb50fac67732dea4a811ea
https://doi.org/10.1007/978-3-642-03359-9_12
https://doi.org/10.1007/978-3-642-03359-9_12
Autor:
Makarius Wenzel, Stefan Berghofer
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783540851097
AISC/MKM/Calculemus
AISC/MKM/Calculemus
Traditionally a rigorous mathematical document consists of a sequence of definition --- statement --- proof. Taking this basic outline as starting point we investigate how these three categories of text can be represented adequately in the formal lan
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6b5fd85f1bf359b47c51a261a90e954a
https://doi.org/10.1007/978-3-540-85110-3_31
https://doi.org/10.1007/978-3-540-85110-3_31
Autor:
Stefan Berghofer, Christian Urban
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783540710653
TPHOLs
TPHOLs
When reasoning about inductively defined predicates, such as typing judgements or reduction relations, proofs are often done by inversion, that is by a case analysis on the last rule of a derivation. In HOL and other formal frameworks this case analy
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e1eb114000ec05d97a7da63abecfe8f1
https://doi.org/10.1007/978-3-540-71067-7_10
https://doi.org/10.1007/978-3-540-71067-7_10
Publikováno v:
Automated Deduction – CADE-21 ISBN: 9783540735946
CADE
CADE
Inductive definitions and rule inductions are two fundamental reasoning tools in logic and computer science. When inductive definitions involve binders, then Barendregt's variable convention is nearly always employed (explicitly or implicitly) in ord
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::db9cde8208a34d33cc3996cd19d453a3
https://doi.org/10.1007/978-3-540-73595-3_4
https://doi.org/10.1007/978-3-540-73595-3_4