Commit 3e818e4a authored by Rene Thiemann's avatar Rene Thiemann
Browse files

sitegen and metadata for Physical Quantities

parent 2ad0e69218eb
......@@ -9781,3 +9781,25 @@ abstract =
be merged and provide proofs of the various conditions which must hold
for these abstractions to subsume their ungeneralised counterparts. A
Code Generator setup to create executable Scala code is also defined.
[Physical_Quantities]
title = A Sound Type System for Physical Quantities, Units, and Measurements
author = Simon Foster <https://www-users.cs.york.ac.uk/~simonf/>, Burkhart Wolff <https://www.lri.fr/~wolff/>
topic = Mathematics/Physics, Computer science/Programming languages/Type systems
date = 2020-10-20
notify = simon.foster@york.ac.uk, wolff@lri.fr
abstract =
The present Isabelle theory builds a formal model for both the
International System of Quantities (ISQ) and the International System
of Units (SI), which are both fundamental for physics and engineering.
Both the ISQ and the SI are deeply integrated into Isabelle's
type system. Quantities are parameterised by dimension types, which
correspond to base vectors, and thus only quantities of the same
dimension can be equated. Since the underlying "algebra of
quantities" induces congruences on quantity and SI types,
specific tactic support is developed to capture these. Our
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).
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8">
<title>A Sound Type System for Physical Quantities, Units, and Measurements - 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>&nbsp;</p>
<a href="https://www.isa-afp.org/">
<img src="../images/isabelle.png" width="100" height="88" border=0>
</a>
<p>&nbsp;</p>
<p>&nbsp;</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>&nbsp;</p>
<p>&nbsp;</p>
</td>
<!-- Content -->
<td width="80%" valign="top">
<div align="center">
<p>&nbsp;</p>
<h1> <font class="first">A</font>
<font class="first">S</font>ound
<font class="first">T</font>ype
<font class="first">S</font>ystem
for
<font class="first">P</font>hysical
<font class="first">Q</font>uantities,
<font class="first">U</font>nits,
and
<font class="first">M</font>easurements
</h1>
<p>&nbsp;</p>
<table width="80%" class="data">
<tbody>
<tr>
<td class="datahead" width="20%">Title:</td>
<td class="data" width="80%">A Sound Type System for Physical Quantities, Units, and Measurements</td>
</tr>
<tr>
<td class="datahead">
Authors:
</td>
<td class="data">
<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="datahead">Submission date:</td>
<td class="data">2020-10-20</td>
</tr>
<tr>
<td class="datahead" valign="top">Abstract:</td>
<td class="abstract mathjax_process">
The present Isabelle theory builds a formal model for both the
International System of Quantities (ISQ) and the International System
of Units (SI), which are both fundamental for physics and engineering.
Both the ISQ and the SI are deeply integrated into Isabelle's
type system. Quantities are parameterised by dimension types, which
correspond to base vectors, and thus only quantities of the same
dimension can be equated. Since the underlying "algebra of
quantities" induces congruences on quantity and SI types,
specific tactic support is developed to capture these. Our
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).</td>
</tr>
<tr>
<td class="datahead" valign="top">BibTeX:</td>
<td class="formatted">
<pre>@article{Physical_Quantities-AFP,
author = {Simon Foster and Burkhart Wolff},
title = {A Sound Type System for Physical Quantities, Units, and Measurements},
journal = {Archive of Formal Proofs},
month = oct,
year = 2020,
note = {\url{http://isa-afp.org/entries/Physical_Quantities.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/Physical_Quantities/outline.pdf">Proof outline</a><br>
<a href="../browser_info/current/AFP/Physical_Quantities/document.pdf">Proof document</a>
</td>
</tr>
<tr>
<td class="links">
<a href="../browser_info/current/AFP/Physical_Quantities/index.html">Browse theories</a>
</td></tr>
<tr>
<td class="links">
<a href="../release/afp-Physical_Quantities-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
......@@ -88,6 +88,15 @@ of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/jour
<tr>
<td class="head">2020</td>
</tr>
<tr>
<td class="entry">
2020-10-20: <a href="entries/Physical_Quantities.html">A Sound Type System for Physical Quantities, Units, and Measurements</a>
<br>
Authors:
<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-09-16: <a href="entries/Syntax_Independent_Logic.html">Syntax-Independent Logic Infrastructure</a>
......
......@@ -9,7 +9,28 @@
and larger scientific developments, mechanically checked
in the theorem prover Isabelle.
</description>
<pubDate>16 Sep 2020 00:00:00 +0000</pubDate>
<pubDate>20 Oct 2020 00:00:00 +0000</pubDate>
<item>
<title>A Sound Type System for Physical Quantities, Units, and Measurements</title>
<link>https://www.isa-afp.org/entries/Physical_Quantities.html</link>
<guid>https://www.isa-afp.org/entries/Physical_Quantities.html</guid>
<dc:creator> Simon Foster, Burkhart Wolff </dc:creator>
<pubDate>20 Oct 2020 00:00:00 +0000</pubDate>
<description>
The present Isabelle theory builds a formal model for both the
International System of Quantities (ISQ) and the International System
of Units (SI), which are both fundamental for physics and engineering.
Both the ISQ and the SI are deeply integrated into Isabelle&#39;s
type system. Quantities are parameterised by dimension types, which
correspond to base vectors, and thus only quantities of the same
dimension can be equated. Since the underlying &#34;algebra of
quantities&#34; induces congruences on quantity and SI types,
specific tactic support is developed to capture these. Our
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>Syntax-Independent Logic Infrastructure</title>
<link>https://www.isa-afp.org/entries/Syntax_Independent_Logic.html</link>
......@@ -601,31 +622,5 @@ and in this setting, we show an instance of Picard-Lindelöf’s
theorem for affine systems of ODEs. Finally, we use this formalisation
to verify three simple hybrid programs.</description>
</item>
<item>
<title>Authenticated Data Structures As Functors</title>
<link>https://www.isa-afp.org/entries/ADS_Functor.html</link>
<guid>https://www.isa-afp.org/entries/ADS_Functor.html</guid>
<dc:creator> Andreas Lochbihler, Ognjen Marić </dc:creator>
<pubDate>16 Apr 2020 00:00:00 +0000</pubDate>
<description>
Authenticated data structures allow several systems to convince each
other that they are referring to the same data structure, even if each
of them knows only a part of the data structure. Using inclusion
proofs, knowledgeable systems can selectively share their knowledge
with other systems and the latter can verify the authenticity of what
is being shared. In this article, we show how to modularly define
authenticated data structures, their inclusion proofs, and operations
thereon as datatypes in Isabelle/HOL, using a shallow embedding.
Modularity allows us to construct complicated trees from reusable
building blocks, which we call Merkle functors. Merkle functors
include sums, products, and function spaces and are closed under
composition and least fixpoints. As a practical application, we model
the hierarchical transactions of &lt;a
href=&#34;https://www.canton.io&#34;&gt;Canton&lt;/a&gt;, a
practical interoperability protocol for distributed ledgers, as
authenticated data structures. This is a first step towards
formalizing the Canton protocol and verifying its integrity and
security guarantees.</description>
</item>
</channel>
</rss>
This diff is collapsed.
......@@ -366,6 +366,7 @@
<a href="entries/Strong_Security.html">Strong_Security</a> &nbsp;
<a href="entries/WHATandWHERE_Security.html">WHATandWHERE_Security</a> &nbsp;
<a href="entries/VolpanoSmith.html">VolpanoSmith</a> &nbsp;
<a href="entries/Physical_Quantities.html">Physical_Quantities</a> &nbsp;
<strong>Logics:</strong>
<a href="entries/ConcurrentIMP.html">ConcurrentIMP</a> &nbsp;
<a href="entries/Refine_Monadic.html">Refine_Monadic</a> &nbsp;
......@@ -867,6 +868,7 @@
<div class="list">
<a href="entries/No_FTL_observers.html">No_FTL_observers</a> &nbsp;
<a href="entries/Safe_Distance.html">Safe_Distance</a> &nbsp;
<a href="entries/Physical_Quantities.html">Physical_Quantities</a> &nbsp;
</div>
<h3>Misc</h3>
<div class="list">
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment