/seL4-l4v-master/HOL4/Manual/Logic/ |
H A D | Makefile | 14 ps: logic.ps 15 pdf: logic.pdf 18 rm -f *.dvi *.aux *.toc *.log *.bbl *.blg logic.pdf logic.ps 20 logic.pdf: logic.tex $(CHAPTERS) $(OTHER) 21 ${PDFLATEX} logic 22 ${BIBTEX} logic 23 ${PDFLATEX} logic 24 ${PDFLATEX} logic [all...] |
H A D | syntax.tex | 7 \chapter{Syntax and Semantics}\label{logic} 13 logic supported by the \HOL{} system, which is a variant of 15 will henceforth be called the \HOL{} logic, or just \HOL. The 18 of this description is the \HOL{} logic. Note that there is a 20 logic, namely the programming language \ML. This is the language used 21 to manipulate the \HOL{} logic by users of the system. It is hoped 35 universe\/}\index{universe, in semantics of HOL logic@universe, in 36 semantics of \HOL{} logic} and which is assumed to have the following 106 \theory{ZFC} set theory of the semantics of the \HOL{} logic to be given 112 The types\index{type constraint!in HOL logic [all...] |
H A D | preface.tex | 4 This volume contains the description of the \HOL\ system's logic. It 8 \item \LOGIC: a formal description of the higher order logic 19 logic in terms of a set-theoretic semantics. This material was 21 \DESCRIPTION. Because this logic is shared with other theorem-proving 27 higher order logic (hence the acronym `\HOL'). To this end, the formal 28 logic is interfaced to a general purpose programming language (\ML, for 29 meta-language) in which terms and theorems of the logic can be denoted, 31 The version of higher order logic used in \HOL\ is predicate calculus 36 (The use of higher order logic for this purpose was first advocated by 37 Keith Hanna \cite{Hanna-Daeche}.) However, the logic doe [all...] |
/seL4-l4v-master/isabelle/src/Pure/ML/ |
H A D | ml_console.scala | 19 var logic = Isabelle_System.getenv("ISABELLE_LOGIC") 31 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) 37 Build a logic session image and run the raw Isabelle ML process 43 "l:" -> (arg => logic = arg), 53 // build logic 58 Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs) 65 ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true, 72 options, logic, dir [all...] |
/seL4-l4v-master/l4v/isabelle/src/Pure/ML/ |
H A D | ml_console.scala | 19 var logic = Isabelle_System.getenv("ISABELLE_LOGIC") 31 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) 37 Build a logic session image and run the raw Isabelle ML process 43 "l:" -> (arg => logic = arg), 53 // build logic 58 Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs) 65 ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true, 72 options, logic, dir [all...] |
/seL4-l4v-master/HOL4/Manual/ |
H A D | Makefile | 19 Logic/logic.pdf: 44 logic: Logic/logic.pdf 50 all: description tutorial logic reference interaction quick
|
/seL4-l4v-master/graph-refine/example/ |
H A D | target.py | 12 import logic namespace 34 pair = logic.mk_pairing (functions, f, f2)
|
/seL4-l4v-master/graph-refine/loop-example/synth/ |
H A D | target.py | 12 import logic namespace 34 pair = logic.mk_pairing (functions, f, f2)
|
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | build_docker.scala | 28 logic: String = default_logic, 69 perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \ 70 Isabelle/bin/isabelle build -o system_heaps -b """ + logic + """ && \ 107 var logic = default_logic 123 -l NAME default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """) 130 Build Isabelle docker image with default logic image, using a standard 140 "l:" -> (arg => logic = arg), 154 build_docker(new Console_Progress(), app_archive, base = base, logic = logic,
|
H A D | update.scala | 12 def update(options: Options, logic: String, 23 context.build_logic(logic) 41 context.sessions(logic, log = log).foreach(_.process((args: Dump.Args) => 75 var logic = Dump.default_logic 89 -b NAME base logic image (default """ + isabelle.quote(Dump.default_logic) + """) 104 "b:" -> (arg => logic = arg), 117 update(options, logic,
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | build_docker.scala | 28 logic: String = default_logic, 69 perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \ 70 Isabelle/bin/isabelle build -o system_heaps -b """ + logic + """ && \ 107 var logic = default_logic 123 -l NAME default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """) 130 Build Isabelle docker image with default logic image, using a standard 140 "l:" -> (arg => logic = arg), 154 build_docker(new Console_Progress(), app_archive, base = base, logic = logic,
|
H A D | update.scala | 12 def update(options: Options, logic: String, 23 context.build_logic(logic) 41 context.sessions(logic, log = log).foreach(_.process((args: Dump.Args) => 75 var logic = Dump.default_logic 89 -b NAME base logic image (default """ + isabelle.quote(Dump.default_logic) + """) 104 "b:" -> (arg => logic = arg), 117 update(options, logic,
|
/seL4-l4v-master/HOL4/examples/ind_def/ |
H A D | milScript.sml | 4 (* logic, and proves the Curry-Howard isomorphism for *) 5 (* this and typed combinatory logic. *) 24 (* Combinatory logic types and type judgements. *) 35 (* Definition of well-typed terms of combinatory logic. *) 49 (* Mimimal intuitionistic logic. We now reinterpret -> as implication, *) 50 (* types P:('a)ty as terms of the logic (i.e. propositions), and define a *) 52 (* inductively by the proof rules for the logic. *)
|
/seL4-l4v-master/isabelle/src/Pure/System/ |
H A D | isabelle_process.scala | 17 logic: String = "", 31 Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes, 38 logic: String = "", 55 ML_Process(channel_options, logic = logic, args = args, dirs = dirs, modes = modes,
|
/seL4-l4v-master/l4v/isabelle/src/Pure/System/ |
H A D | isabelle_process.scala | 17 logic: String = "", 31 Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes, 38 logic: String = "", 55 ML_Process(channel_options, logic = logic, args = args, dirs = dirs, modes = modes,
|
/seL4-l4v-master/isabelle/src/Tools/VSCode/src/ |
H A D | build_vscode.scala | 22 val logic = Grammar.default_logic 23 val keywords = Sessions.base_info(options, logic).check_base.overall_syntax.keywords 25 val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
|
H A D | grammar.scala | 19 def default_output(logic: String = ""): String = 20 if (logic == "" || logic == default_logic) "isabelle-grammar.json" 21 else "isabelle-" + logic + "-grammar.json" 140 var logic = default_logic 148 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) 154 "l:" -> (arg => logic = arg), 161 Sessions.base_info(Options.init(), logic, dirs = dirs).check_base.overall_syntax.keywords 162 val output_path = output getOrElse Path.explode(default_output(logic))
|
/seL4-l4v-master/l4v/isabelle/src/Tools/VSCode/src/ |
H A D | build_vscode.scala | 22 val logic = Grammar.default_logic 23 val keywords = Sessions.base_info(options, logic).check_base.overall_syntax.keywords 25 val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
|
H A D | grammar.scala | 19 def default_output(logic: String = ""): String = 20 if (logic == "" || logic == default_logic) "isabelle-grammar.json" 21 else "isabelle-" + logic + "-grammar.json" 140 var logic = default_logic 148 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(default_logic) + """) 154 "l:" -> (arg => logic = arg), 161 Sessions.base_info(Options.init(), logic, dirs = dirs).check_base.overall_syntax.keywords 162 val output_path = output getOrElse Path.explode(default_output(logic))
|
/seL4-l4v-master/graph-refine/loop-example/O1/ |
H A D | target.py | 14 import logic namespace 33 assert logic.aligned_address_sanity (afunctions, symbols, 4)
|
/seL4-l4v-master/graph-refine/seL4-example/ |
H A D | target.py | 14 import logic namespace 31 assert logic.aligned_address_sanity (afunctions, symbols, 4) 41 print 'Doing stack/inst logic.'
|
/seL4-l4v-master/graph-refine/loop-example/O2/ |
H A D | target.py | 14 import logic namespace 33 assert logic.aligned_address_sanity (afunctions, symbols, 4)
|
/seL4-l4v-master/HOL4/examples/Hoare-for-divergence/ |
H A D | std_logicScript.sml | 5 (* -- inference rules for a standard total-correctness Hoare logic -- *)
|
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/ |
H A D | dataabs.ml | 5 % logic to boolean logic for single bits and for % 10 % logic to booleans. The predicates Def and Defn % 12 % ways of abstracting to boolean logic would include % 14 % three-valued logic consisting of T,F and bottom. %
|
/seL4-l4v-master/HOL4/Manual/Description/ |
H A D | preface.tex | 8 \item \LOGIC: a formal description of the higher order logic 23 higher order logic (hence the acronym `\HOL'). To this end, the formal 24 logic is interfaced to a general purpose programming language (\ML, for 25 meta-language) in which terms and theorems of the logic can be denoted, 27 The version of higher order logic used in \HOL\ is predicate calculus 32 (The use of higher order logic for this purpose was first advocated by 33 Keith Hanna \cite{Hanna-Daeche}.) However, the logic does not restrict 36 This document presents the \HOL\ logic in its \ML{} guise, and 38 generate proofs in the logic. Thus, it describes how the abstract 45 the language \ML. That work centred on a system called \LCF\ (logic fo [all...] |