Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
isa-afp
afp-2020
Commits
b33e4e32b4ec
Commit
84dcc3bb
authored
Dec 02, 2020
by
Gerwin Klein
Browse files
merge
parents
ab7cbd1a97a5
5728774bf660
Changes
10
Expand all
Hide whitespace changes
Inline
Side-by-side
metadata/metadata
View file @
b33e4e32
...
...
@@ -7552,7 +7552,7 @@ abstract =
[Verified_SAT_Based_AI_Planning]
title = Verified SAT-Based AI Planning
author = Mohammad Abdulaziz <http://home.in.tum.de/~mansour/>, Friedrich Kurz
author = Mohammad Abdulaziz <http://home.in.tum.de/~mansour/>, Friedrich Kurz
<>
topic = Computer science/Artificial intelligence
date = 2020-10-29
notify = mohammad.abdulaziz8@gmail.com
...
...
@@ -9912,7 +9912,7 @@ author = Anthony Bordg <mailto:apdb3@cam.ac.uk>, Hanna Lachnitt<mailto:lachnitt@
topic = Computer science/Algorithms/Quantum computing, Mathematics/Physics/Quantum information
date = 2020-11-22
notify = apdb3@cam.ac.uk, lachnitt@stanford.edu
abstract =
abstract =
This work is an effort to formalise some quantum algorithms and
results in quantum information theory. Formal methods being critical
for the safety and security of algorithms and protocols, we foresee
...
...
@@ -9923,3 +9923,13 @@ abstract =
algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner's
Dilemma.
[Finite-Map-Extras]
title = Finite Map Extras
author = Javier Díaz <mailto:javier.diaz.manzi@gmail.com>
topic = Computer science/Data structures
date = 2020-10-12
notify = javier.diaz.manzi@gmail.com
abstract =
This entry includes useful syntactic sugar, new operators and functions, and
their associated lemmas for finite maps which currently are not
present in the standard Finite_Map theory.
thys/Finite-Map-Extras/Finite_Map_Extras.thy
0 → 100644
View file @
b33e4e32
This diff is collapsed.
Click to expand it.
thys/Finite-Map-Extras/ROOT
0 → 100644
View file @
b33e4e32
chapter AFP
session "Finite-Map-Extras" (AFP) = HOL +
options [timeout = 600]
sessions
"HOL-Library"
theories
Finite_Map_Extras
document_files
"root.tex"
thys/Finite-Map-Extras/document/root.tex
0 → 100644
View file @
b33e4e32
\documentclass
[11pt,a4paper]
{
article
}
\usepackage
{
isabelle,isabellesym
}
\usepackage
{
latexsym
}
\usepackage
{
amssymb
}
\usepackage
{
pdfsetup
}
\addtolength
{
\hoffset
}{
-1,5cm
}
\addtolength
{
\textwidth
}{
3cm
}
%\urlstyle{rm}
\isabellestyle
{
it
}
\begin{document}
\title
{
Finite Map Extras
}
\author
{
Javier D
\'
iaz
\\\url
{
<javier.diaz.manzi@gmail.com>
}}
\maketitle
\begin{abstract}
This includes useful syntactic sugar, new operators and functions and their associated lemmas for
finite maps which currently are not present in the standard
\texttt
{
Finite
\_
Map
}
theory.
\end{abstract}
\tableofcontents
\parindent
0pt
\parskip
0.5ex
\input
{
session
}
\end{document}
thys/ROOTS
View file @
b33e4e32
...
...
@@ -164,6 +164,7 @@ FileRefinement
FinFun
Finger-Trees
Finite_Automata_HF
Finite-Map-Extras
First_Order_Terms
First_Welfare_Theorem
Fishburn_Impossibility
...
...
web/entries/Finite-Map-Extras.html
0 → 100644
View file @
b33e4e32
<!DOCTYPE html>
<html
lang=
"en"
>
<head>
<meta
charset=
"utf-8"
>
<title>
Finite Map Extras - Archive of Formal Proofs
</title>
<link
rel=
"stylesheet"
type=
"text/css"
href=
"../front.css"
>
<link
rel=
"icon"
href=
"../images/favicon.ico"
type=
"image/icon"
>
<link
rel=
"alternate"
type=
"application/rss+xml"
title=
"RSS"
href=
"../rss.xml"
>
<!-- MathJax for LaTeX support in abstracts -->
<script>
MathJax
=
{
tex
:
{
inlineMath
:
[[
'
$
'
,
'
$
'
],
[
'
\\
(
'
,
'
\\
)
'
]]
},
processEscapes
:
true
,
svg
:
{
fontCache
:
'
global
'
}
};
</script>
<script
id=
"MathJax-script"
async
src=
"../components/mathjax/es5/tex-mml-chtml.js"
></script>
</head>
<body
class=
"mathjax_ignore"
>
<table
width=
"100%"
>
<tbody>
<tr>
<!-- Navigation -->
<td
width=
"20%"
align=
"center"
valign=
"top"
>
<p>
</p>
<a
href=
"https://www.isa-afp.org/"
>
<img
src=
"../images/isabelle.png"
width=
"100"
height=
"88"
border=
0
>
</a>
<p>
</p>
<p>
</p>
<table
class=
"nav"
width=
"80%"
>
<tr>
<td
class=
"nav"
width=
"100%"
><a
href=
"../index.html"
>
Home
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../about.html"
>
About
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../submitting.html"
>
Submission
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../updating.html"
>
Updating Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../using.html"
>
Using Entries
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../search.html"
>
Search
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../statistics.html"
>
Statistics
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../topics.html"
>
Index
</a></td>
</tr>
<tr>
<td
class=
"nav"
><a
href=
"../download.html"
>
Download
</a></td>
</tr>
</table>
<p>
</p>
<p>
</p>
</td>
<!-- Content -->
<td
width=
"80%"
valign=
"top"
>
<div
align=
"center"
>
<p>
</p>
<h1>
<font
class=
"first"
>
F
</font>
inite
<font
class=
"first"
>
M
</font>
ap
<font
class=
"first"
>
E
</font>
xtras
</h1>
<p>
</p>
<table
width=
"80%"
class=
"data"
>
<tbody>
<tr>
<td
class=
"datahead"
width=
"20%"
>
Title:
</td>
<td
class=
"data"
width=
"80%"
>
Finite Map Extras
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Author:
</td>
<td
class=
"data"
>
Javier Díaz (javier /dot/ diaz /dot/ manzi /at/ gmail /dot/ com)
</td>
</tr>
<tr>
<td
class=
"datahead"
>
Submission date:
</td>
<td
class=
"data"
>
2020-10-12
</td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
Abstract:
</td>
<td
class=
"abstract mathjax_process"
>
This entry includes useful syntactic sugar, new operators and functions, and
their associated lemmas for finite maps which currently are not
present in the standard Finite_Map theory.
</td>
</tr>
<tr>
<td
class=
"datahead"
valign=
"top"
>
BibTeX:
</td>
<td
class=
"formatted"
>
<pre>
@article{Finite-Map-Extras-AFP,
author = {Javier Díaz},
title = {Finite Map Extras},
journal = {Archive of Formal Proofs},
month = oct,
year = 2020,
note = {\url{http://isa-afp.org/entries/Finite-Map-Extras.html},
Formal proof development},
ISSN = {2150-914x},
}
</pre>
</td>
</tr>
<tr><td
class=
"datahead"
>
License:
</td>
<td
class=
"data"
><a
href=
"http://isa-afp.org/LICENSE"
>
BSD License
</a></td></tr>
</tbody>
</table>
<p></p>
<table
class=
"links"
>
<tbody>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/Finite-Map-Extras/outline.pdf"
>
Proof outline
</a><br>
<a
href=
"../browser_info/current/AFP/Finite-Map-Extras/document.pdf"
>
Proof document
</a>
</td>
</tr>
<tr>
<td
class=
"links"
>
<a
href=
"../browser_info/current/AFP/Finite-Map-Extras/index.html"
>
Browse theories
</a>
</td></tr>
<tr>
<td
class=
"links"
>
<a
href=
"../release/afp-Finite-Map-Extras-current.tar.gz"
>
Download this entry
</a>
</td>
</tr>
<tr><td
class=
"links"
>
Older releases:
None
</td></tr>
</tbody>
</table>
</div>
</td>
</tr>
</tbody>
</table>
<script
src=
"../jquery.min.js"
></script>
<script
src=
"../script.js"
></script>
</body>
</html>
\ No newline at end of file
web/index.html
View file @
b33e4e32
...
...
@@ -124,6 +124,14 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
<a
href=
"https://www-users.cs.york.ac.uk/~simonf/"
>
Simon Foster
</a>
and
<a
href=
"https://www.lri.fr/~wolff/"
>
Burkhart Wolff
</a>
</td>
</tr>
<tr>
<td
class=
"entry"
>
2020-10-12:
<a
href=
"entries/Finite-Map-Extras.html"
>
Finite Map Extras
</a>
<br>
Author:
Javier Díaz
</td>
</tr>
<tr>
<td
class=
"entry"
>
...
...
web/rss.xml
View file @
b33e4e32
...
...
@@ -79,6 +79,17 @@ construction is validated by a test-set of known equivalences between
both quantities and SI units. Moreover, the presented theory can be
used for type-safe conversions between the SI system and others, like
the British Imperial System (BIS).
</description>
</item>
<item>
<title>
Finite Map Extras
</title>
<link>
https://www.isa-afp.org/entries/Finite-Map-Extras.html
</link>
<guid>
https://www.isa-afp.org/entries/Finite-Map-Extras.html
</guid>
<dc:creator>
Javier Díaz
</dc:creator>
<pubDate>
12 Oct 2020 00:00:00 +0000
</pubDate>
<description>
This entry includes useful syntactic sugar, new operators and functions, and
their associated lemmas for finite maps which currently are not
present in the standard Finite_Map theory.
</description>
</item>
<item>
<title>
A Formal Model of the Safely Composable Document Object Model with Shadow Roots
</title>
...
...
@@ -583,17 +594,5 @@ syntactic normalisation procedure for LTL yielding a normal form,
comparable to the one by Chang, Manna, and Pnueli, that has only a
single exponential blow-up.
</description>
</item>
<item>
<title>
Formalization of Forcing in Isabelle/ZF
</title>
<link>
https://www.isa-afp.org/entries/Forcing.html
</link>
<guid>
https://www.isa-afp.org/entries/Forcing.html
</guid>
<dc:creator>
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
</dc:creator>
<pubDate>
06 May 2020 00:00:00 +0000
</pubDate>
<description>
We formalize the theory of forcing in the set theory framework of
Isabelle/ZF. Under the assumption of the existence of a countable
transitive model of ZFC, we construct a proper generic extension and
show that the latter also satisfies ZFC.
</description>
</item>
</channel>
</rss>
web/statistics.html
View file @
b33e4e32
This diff is collapsed.
Click to expand it.
web/topics.html
View file @
b33e4e32
...
...
@@ -291,6 +291,7 @@
<a
href=
"entries/Interval_Arithmetic_Word32.html"
>
Interval_Arithmetic_Word32
</a>
<a
href=
"entries/ADS_Functor.html"
>
ADS_Functor
</a>
<a
href=
"entries/Relational_Disjoint_Set_Forests.html"
>
Relational_Disjoint_Set_Forests
</a>
<a
href=
"entries/Finite-Map-Extras.html"
>
Finite-Map-Extras
</a>
</div>
<h3>
Functional programming
</h3>
<div
class=
"list"
>
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment